English
For a finite index set s, the weighted order of the product ∏_{i∈s} f_i equals the sum of the weighted orders: weightedOrder w (∏ i∈s f_i) = ∑ i∈s weightedOrder w (f_i).
Русский
Для конечного множества индексов s взвешенный порядок произведения ∏_{i∈s} f_i равен сумме взвешенных порядков: weightedOrder w (∏ i∈s f_i) = ∑ i∈s weightedOrder w (f_i).
LaTeX
$$$\mathrm{weightedOrder}\,w\Big(\prod_{i\in s} f_i\Big)=\sum_{i\in s}\mathrm{weightedOrder}\,w(f_i).$$$
Lean4
theorem weightedOrder_prod {R : Type*} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type*} (w : σ → ℕ)
(f : ι → MvPowerSeries σ R) (s : Finset ι) : (∏ i ∈ s, f i).weightedOrder w = ∑ i ∈ s, (f i).weightedOrder w := by
induction s using Finset.cons_induction with
| empty => simp
| cons a s ha ih => rw [Finset.sum_cons ha, Finset.prod_cons ha, weightedOrder_mul, ih]
