Commit 2025-10-22 20:30 71a105d7

feat(Analysis/SpecialFunctions/Log): log_prod for Lists and Multisets (#30681) We add

lemma log_list_prod {l : List ℝ} (h : ∀ x ∈ l, x ≠ 0) :  log l.prod = (l.map (fun x ↦ log x)).sum

and

lemma log_multiset_prod {s : Multiset ℝ} (h : ∀ x ∈ s, x ≠ 0) :  log s.prod = (s.map (fun x ↦ log x)).sum