English
The log of a finite product equals the sum of logs of the factors, provided all factors are nonzero.
Русский
Логарифм произведения конечного числа множителей равен сумме логарифмов этих множителей при условии их ненулевости.
LaTeX
$$$\log_b b\ (\prod_{i\in s} f_i) = \sum_{i\in s} \log_b b (f_i)$$$
Lean4
theorem logb_prod {α : Type*} (s : Finset α) (f : α → ℝ) (hf : ∀ x ∈ s, f x ≠ 0) :
logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i) := by
induction s using Finset.cons_induction_on with
| empty => simp
| cons => simp_all [logb_mul, Finset.prod_ne_zero_iff]