English
For any f and n, X^n divides f if and only if f.coeff d = 0 for all d < n.
Русский
Для любого f и n, X^n делит f тогда и только тогда, когда коэффициенты f при степенях d < n равны нулю.
LaTeX
$$$X^n \mid f \iff \forall d < n, f.coeff d = 0$$$
Lean4
theorem X_pow_dvd_iff {f : R[X]} {n : ℕ} : X ^ n ∣ f ↔ ∀ d < n, f.coeff d = 0 :=
⟨fun ⟨g, hgf⟩ d hd => by simp only [hgf, coeff_X_pow_mul', ite_eq_right_iff, not_le_of_gt hd, IsEmpty.forall_iff],
fun hd => by
induction n with
| zero => simp [pow_zero]
| succ n hn =>
obtain ⟨g, hgf⟩ := hn fun d : ℕ => fun H : d < n => hd _ (Nat.lt_succ_of_lt H)
have := coeff_X_pow_mul g n 0
rw [zero_add, ← hgf, hd n (Nat.lt_succ_self n)] at this
obtain ⟨k, hgk⟩ := Polynomial.X_dvd_iff.mpr this.symm
use k
rwa [pow_succ, mul_assoc, ← hgk]⟩
