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)]