X_dvd_iff — Mathlib

English

For any polynomial f, X divides f if and only if the constant term f.coeff 0 equals 0.

Русский

Для любого многочлена f, X делит f тогда и только тогда, когда константный коэффициент f.coeff 0 равен 0.

LaTeX

$$$X \mid f \iff f.coeff 0 = 0$$$

Lean4

theorem X_dvd_iff {f : R[X]} : X ∣ f ↔ f.coeff 0 = 0 :=
  ⟨fun ⟨g, hfg⟩ => by rw [hfg, coeff_X_mul_zero], fun hf =>
    ⟨f.divX, by rw [← add_zero (X * f.divX), ← C_0, ← hf, X_mul_divX_add]⟩⟩

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