English
Let φ_i be a finite family of formal power series indexed by a finite set s. The order of the product ∏_{i∈s} φ_i equals the sum of their orders.
Русский
Пусть φ_i — конечная семейство формальных степенных рядов, индексируемая по конечному множеству s. Порядок произведения ∏_{i∈s} φ_i равен сумме их порядков.
LaTeX
$$$ \\operatorname{order}\\left( \\prod_{i \\in s} \\phi(i) \\right) = \\sum_{i \\in s} \\operatorname{order}(\\phi(i)) $$$
Lean4
theorem order_prod {R : Type*} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type*} (φ : ι → R⟦X⟧)
(s : Finset ι) : (∏ i ∈ s, φ i).order = ∑ i ∈ s, (φ i).order := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha ih => rw [Finset.sum_cons ha, Finset.prod_cons ha, order_mul, ih]
