English
A polynomial P is nilpotent if and only if all its coefficients are nilpotent.
Русский
Полином P нильпотентен тогда и только тогда, когда все его коэффициенты нильпотентны.
LaTeX
$$IsNilpotent(P) ↔ ∀ i, IsNilpotent(coeff(P,i))$$
Lean4
protected theorem isNilpotent_iff : IsNilpotent P ↔ ∀ i, IsNilpotent (coeff P i) :=
by
refine ⟨P.recOnHorner (by simp) (fun p r hp₀ _ hp hpr i ↦ ?_) (fun p _ hnp hpX i ↦ ?_), fun h ↦ ?_⟩
· rw [← sum_monomial_eq P]
exact isNilpotent_sum (fun i _ ↦ by simpa only [isNilpotent_monomial_iff] using h i)
· have hr : IsNilpotent (C r) := by
obtain ⟨k, hk⟩ := hpr
replace hp : eval 0 p = 0 := by rwa [coeff_zero_eq_aeval_zero] at hp₀
refine isNilpotent_C_iff.mpr ⟨k, ?_⟩
simpa [coeff_zero_eq_aeval_zero, hp] using congr_arg (fun q ↦ coeff q 0) hk
rcases i with - | i
· simpa [hp₀] using hr
simp only [coeff_add, coeff_C_succ, add_zero]
apply hp
simpa using Commute.isNilpotent_sub (Commute.all _ _) hpr hr
· rcases i with - | i
· simp
simpa using hnp (isNilpotent_mul_X_iff.mp hpX) i
