English
Let R be a commutative ring and P a polynomial in R[X]. If the constant term P(0) is a unit and every other coefficient P.i for i ≠ 0 is nilpotent, then P is a unit in R[X].
Русский
Пусть R — коммутативное кольцо, а P — многочлен из R[X]. Если постоянный член P(0) является единицей, а все остальные коэффициенты P.i при i ≠ 0 нильпотентны, то P является единицей в R[X].
LaTeX
$$$\Bigl( \operatorname{IsUnit}(P.\text{coeff }0) \land \forall i \,(i \neq 0 \rightarrow \operatorname{IsNilpotent}(P.\text{coeff }i)) \Bigr) \Rightarrow \operatorname{IsUnit}(P)$$$
Lean4
/-- Let `P` be a polynomial over `R`. If its constant term is a unit and its other coefficients are
nilpotent, then `P` is a unit.
See also `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent`. -/
theorem isUnit_of_coeff_isUnit_isNilpotent (hunit : IsUnit (P.coeff 0)) (hnil : ∀ i, i ≠ 0 → IsNilpotent (P.coeff i)) :
IsUnit P :=
by
induction h : P.natDegree using Nat.strong_induction_on generalizing P with
| _ k hind
by_cases hdeg : P.natDegree = 0
· rw [eq_C_of_natDegree_eq_zero hdeg]
exact hunit.map C
set P₁ := P.eraseLead with hP₁
suffices IsUnit P₁
by
rw [← eraseLead_add_monomial_natDegree_leadingCoeff P, ← C_mul_X_pow_eq_monomial, ← hP₁]
refine IsNilpotent.isUnit_add_left_of_commute ?_ this (Commute.all _ _)
exact isNilpotent_C_mul_pow_X_of_isNilpotent _ (hnil _ hdeg)
have hdeg₂ := lt_of_le_of_lt P.eraseLead_natDegree_le (Nat.sub_lt (Nat.pos_of_ne_zero hdeg) zero_lt_one)
refine hind P₁.natDegree ?_ ?_ (fun i hi => ?_) rfl
· simp_rw [P₁, ← h, hdeg₂]
· simp_rw [P₁, eraseLead_coeff_of_ne _ (Ne.symm hdeg), hunit]
· by_cases H : i ≤ P₁.natDegree
· simp_rw [P₁, eraseLead_coeff_of_ne _ (ne_of_lt (lt_of_le_of_lt H hdeg₂)), hnil i hi]
· simp_rw [coeff_eq_zero_of_natDegree_lt (lt_of_not_ge H), IsNilpotent.zero]
