coeff_mul_prod_one_sub_of_lt_order

English

For a finite set s, if deg(d) < ord(1 - g_i) for all i in s, then the coefficient of d in f multiplied by the product over s of (1 - g_i) equals the coefficient of d in f.

Русский

Если deg(d) < ord(1 - g_i) для каждого i в s, то коэффициент d в f·∏_{i∈s}(1 - g_i) равен коэффициенту d в f.

LaTeX

$$$ \forall i \in s, \operatorname{degree} d < \operatorname{ord}(1 - g_i) \Rightarrow \operatorname{coeff}_d\left(f \cdot \prod_{i\in s} (1 - g_i)\right) = \operatorname{coeff}_d f $$$

Lean4

theorem coeff_mul_prod_one_sub_of_lt_order {R ι : Type*} [CommRing R] (d : σ →₀ ℕ) (s : Finset ι)
    (f : MvPowerSeries σ R) (g : ι → MvPowerSeries σ R) :
    (∀ i ∈ s, degree d < order (g i)) → coeff d (f * ∏ i ∈ s, (1 - g i)) = coeff d f :=
  by
  rw [degree_eq_weight_one]
  exact coeff_mul_prod_one_sub_of_lt_weightedOrder _ d s f g

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