Documentation

Mathlib.Algebra.Polynomial.Degree.Units

Degree of polynomials that are units #

theorem Polynomial.isUnit_iff {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} :
IsUnit p ∃ (r : R), IsUnit r C r = p

Characterization of a unit of a polynomial ring over an integral domain R. See Polynomial.isUnit_iff_coeff_isUnit_isNilpotent when R is a commutative ring.

theorem Polynomial.Monic.C_dvd_iff_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) {a : R} :
C a p IsUnit a