X_pow_dvd_iff — Mathlib

English

For φ ∈ R⟦X⟧, X^n divides φ if and only if all coefficients of φ below degree n vanish.

Русский

Для φ ∈ R⟦X⟧, X^n делит φ тогда и только тогда все коэффициенты φ меньшие n равны нулю.

LaTeX

$$$(X)^n \mid \phi \quad\Longleftrightarrow\quad \forall m < n,\; \operatorname{coeff}_m(\phi) = 0$$$

Lean4

theorem X_pow_dvd_iff {n : ℕ} {φ : R⟦X⟧} : (X : R⟦X⟧) ^ n ∣ φ ↔ ∀ m, m < n → coeff m φ = 0 :=
  by
  convert @MvPowerSeries.X_pow_dvd_iff Unit R _ () n φ
  constructor <;> intro h m hm
  · rw [Finsupp.unique_single m]
    convert h _ hm
  · apply h
    simpa only [Finsupp.single_eq_same] using hm

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