order_prod — Mathlib

English

For a finite set s, the order of the product ∏_{i∈s} f_i equals the sum of the orders: (∏_{i∈s} f_i).order = ∑_{i∈s} (f_i).order.

Русский

Для конечного множества s порядок произведения равен сумме порядков.

LaTeX

$$$\bigl(\prod_{\,i\in s} f_i\bigr).\mathrm{order = }\sum_{i\in s} (f_i).\mathrm{order}.$$$

Lean4

theorem order_prod {R : Type*} [CommSemiring R] [NoZeroDivisors R] [Nontrivial R] {ι : Type*}
    (f : ι → MvPowerSeries σ R) (s : Finset ι) : (∏ i ∈ s, f i).order = ∑ i ∈ s, (f i).order :=
  weightedOrder_prod _ _ _

Похожие утверждения