English
Nilpotence of a multivariate polynomial is equivalent to the nilpotence of all its coefficients.
Русский
Нильпотентность многочлена в нескольких переменных эквивалентна нильпотентности всех его коэффициентов.
LaTeX
$$$$ \mathrm{IsNilpotent}(P) \iff \forall i, \mathrm{IsNilpotent}(P_{i}) $$$$
Lean4
theorem isNilpotent_iff : IsNilpotent P ↔ ∀ i, IsNilpotent (P.coeff i) :=
by
obtain ⟨n, f, hf, P, rfl⟩ := P.exists_fin_rename
rw [IsNilpotent.map_iff (rename_injective _ hf), MvPolynomial.isNilpotent_iff_of_fintype]
lift f to Fin n ↪ σ using hf
refine ⟨fun H i ↦ ?_, fun H i ↦ by simpa using H (i.embDomain f)⟩
by_cases H : i ∈ Set.range (Finsupp.embDomain f)
· aesop
· rw [coeff_rename_eq_zero] <;> aesop (add simp Finsupp.embDomain_eq_mapDomain)
