English
X_s divides φ if and only if all coefficients with m(s) = 0 vanish.
Русский
X_s делит φ тогда, когда все коэффициенты с m(s) = 0 равны нулю.
LaTeX
$$$(X_s) \\mid \\phi \\iff ∀ m: σ \\to ℕ, m(s) = 0 \\Rightarrow \\operatorname{coeff} m \\; \\phi = 0$$$
Lean4
theorem X_dvd_iff {s : σ} {φ : MvPowerSeries σ R} :
(X s : MvPowerSeries σ R) ∣ φ ↔ ∀ m : σ →₀ ℕ, m s = 0 → coeff m φ = 0 :=
by
rw [← pow_one (X s : MvPowerSeries σ R), X_pow_dvd_iff]
constructor <;> intro h m hm
· exact h m (hm.symm ▸ zero_lt_one)
· exact h m (Nat.eq_zero_of_le_zero <| Nat.le_of_succ_le_succ hm)