X_dvd_iff — Mathlib

English

X divides φ if and only if the constant term of φ is zero.

Русский

X делит φ тогда и только тогда константный коэффициент φ равен нулю.

LaTeX

$$$X \mid \phi \;\Longleftrightarrow\; \operatorname{constantCoeff}(\phi) = 0$$$

Lean4

theorem X_dvd_iff {φ : R⟦X⟧} : (X : R⟦X⟧) ∣ φ ↔ constantCoeff φ = 0 :=
  by
  rw [← pow_one (X : R⟦X⟧), X_pow_dvd_iff, ← coeff_zero_eq_constantCoeff_apply]
  constructor <;> intro h
  · exact h 0 zero_lt_one
  · intro m hm
    rwa [Nat.eq_zero_of_le_zero (Nat.le_of_succ_le_succ hm)]

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