English
If P is a unit in R[X], then its constant term is a unit and every nonconstant coefficient is nilpotent.
Русский
Если P является единицей в R[X], то её постоянный коэффициент является единицей, и все коэффициенты с положительной степенью нильпотентны.
LaTeX
$$$\operatorname{IsUnit}(P) \Rightarrow \operatorname{IsUnit}(P.\text{coeff }0) \land \forall i \,(i \neq 0 \rightarrow \operatorname{IsNilpotent}(P.\text{coeff }i))$$$
Lean4
/-- Let `P` be a polynomial over `R`. If `P` is a unit, then all its coefficients are nilpotent,
except its constant term which is a unit.
See also `Polynomial.isUnit_iff_coeff_isUnit_isNilpotent`. -/
theorem coeff_isUnit_isNilpotent_of_isUnit (hunit : IsUnit P) :
IsUnit (P.coeff 0) ∧ (∀ i, i ≠ 0 → IsNilpotent (P.coeff i)) :=
by
obtain ⟨Q, hQ⟩ := IsUnit.exists_right_inv hunit
constructor
· refine isUnit_of_mul_eq_one _ (Q.coeff 0) ?_
have h := (mul_coeff_zero P Q).symm
rwa [hQ, coeff_one_zero] at h
· intro n hn
rw [nilpotent_iff_mem_prime]
intro I hI
let f := mapRingHom (Ideal.Quotient.mk I)
have hPQ : degree (f P) = 0 ∧ degree (f Q) = 0 := by
rw [← Nat.WithBot.add_eq_zero_iff, ← degree_mul, ← map_mul, hQ, map_one, degree_one]
have hcoeff : (f P).coeff n = 0 := by
refine coeff_eq_zero_of_degree_lt ?_
rw [hPQ.1]
exact WithBot.coe_pos.2 hn.bot_lt
rw [coe_mapRingHom, coeff_map, ← RingHom.mem_ker, Ideal.mk_ker] at hcoeff
exact hcoeff
