English
For s ∈ σ and φ ∈ MvPowerSeries σ R, (X_s)^n divides φ iff every coefficient corresponding to multi-indices m with m(s) < n vanishes.
Русский
Для X_s степенной серии, (X_s)^n делит φ тогда, когда для каждой компоненты m с m(s) < n соответствующий коэффициент φ равен нулю.
LaTeX
$$$(X_s)^n \\mid \\phi \\;\\Longleftrightarrow\\; \\forall m: \\sigma \\to\\!\\!\\! ℕ,\\ m(s) < n \\Rightarrow \\operatorname{coeff} m \\; \\phi = 0$$$
Lean4
theorem X_pow_dvd_iff {s : σ} {n : ℕ} {φ : MvPowerSeries σ R} :
(X s : MvPowerSeries σ R) ^ n ∣ φ ↔ ∀ m : σ →₀ ℕ, m s < n → coeff m φ = 0 := by
classical
constructor
· rintro ⟨φ, rfl⟩ m h
rw [coeff_mul, Finset.sum_eq_zero]
rintro ⟨i, j⟩ hij
rw [coeff_X_pow, if_neg, zero_mul]
contrapose! h
dsimp at h
subst i
rw [mem_antidiagonal] at hij
rw [← hij, Finsupp.add_apply, Finsupp.single_eq_same]
exact Nat.le_add_right n _
· intro h
refine ⟨fun m => coeff (m + single s n) φ, ?_⟩
ext m
by_cases H : m - single s n + single s n = m
· rw [coeff_mul, Finset.sum_eq_single (single s n, m - single s n)]
· rw [coeff_X_pow, if_pos rfl, one_mul]
simpa using congr_arg (fun m : σ →₀ ℕ => coeff m φ) H.symm
· rintro ⟨i, j⟩ hij hne
rw [mem_antidiagonal] at hij
rw [coeff_X_pow]
split_ifs with hi
· exfalso
apply hne
rw [← hij, ← hi, Prod.mk_inj]
refine ⟨rfl, ?_⟩
ext t
simp only [add_tsub_cancel_left]
· exact zero_mul _
· intro hni
exfalso
apply hni
rwa [mem_antidiagonal, add_comm]
· rw [h, coeff_mul, Finset.sum_eq_zero]
· rintro ⟨i, j⟩ hij
rw [mem_antidiagonal] at hij
rw [coeff_X_pow]
split_ifs with hi
· exfalso
apply H
rw [← hij, hi]
ext
rw [coe_add, coe_add, Pi.add_apply, Pi.add_apply, add_tsub_cancel_left, add_comm]
· exact zero_mul _
· contrapose! H
ext t
by_cases hst : s = t
· subst t
simpa using tsub_add_cancel_of_le H
· simp [hst]
