Theorems · Theorem · commutative algebra

Polynomial.coeff_isUnit_isNilpotent_of_isUnit

∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R},
  IsUnit P → IsUnit (P.coeff 0) ∧ ∀ (i : ℕ), i ≠ 0 → IsNilpotent (P.coeff i)

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.

Defined in

Mathlib.RingTheory.Polynomial.Nilpotent

Cited by

2 results in Mathlib

Foundations

Depth 107 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommRing