X_dvd_iff — Mathlib

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)

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