English
As above, weightedOrder w f = n iff there exists a coefficient of weight n nonzero and all lower weights vanish.
Русский
Как выше, weightedOrder_w(f)=n тогда, когда существует коэффициент весом n не нулевой и все коэффициенты меньшего веса нули.
LaTeX
$$f.weightedOrder w = n ↔ (∃ d, coeff d f ≠ 0 ∧ weight w d = n) ∧ ∀ d, weight w d < n → coeff d f = 0$$
Lean4
theorem coeff_mul_prod_one_sub_of_lt_weightedOrder {R ι : Type*} [CommRing R] (d : σ →₀ ℕ) (s : Finset ι)
(f : MvPowerSeries σ R) (g : ι → MvPowerSeries σ R) (h : ∀ i ∈ s, (weight w d) < weightedOrder w (g i)) :
coeff d (f * ∏ i ∈ s, (1 - g i)) = coeff d f := by
classical
induction s using Finset.induction_on with
| empty => simp only [Finset.prod_empty, mul_one]
| insert a s ha ih =>
simp only [Finset.mem_insert, forall_eq_or_imp] at h
rw [Finset.prod_insert ha, ← mul_assoc, mul_right_comm, coeff_mul_left_one_sub_of_lt_weightedOrder w h.1, ih h.2]
