Documentation

Mathlib.Algebra.Polynomial.Degree.Units

Degree of polynomials that are units #

theorem Polynomial.natDegree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} (h : IsUnit p) :

p.natDegree = 0

theorem Polynomial.degree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} [Nontrivial R] (h : IsUnit p) :

@[simp]

theorem Polynomial.degree_coe_units {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) :

(↑u).degree = 0

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.not_isUnit_of_degree_pos {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < p.degree) :

theorem Polynomial.not_isUnit_of_natDegree_pos {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < p.natDegree) :

@[simp]

theorem Polynomial.natDegree_coe_units {R : Type u} [Semiring R] [NoZeroDivisors R] (u : (Polynomial R)ˣ) :

(↑u).natDegree = 0

theorem Polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) :

(↑u).coeff 0 ≠ 0

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

theorem Polynomial.Monic.degree_pos_of_not_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) :

theorem Polynomial.Monic.natDegree_pos_of_not_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) :

0 < p.natDegree

theorem Polynomial.degree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [CommSemiring R] {a p : Polynomial R} (hp : p.Monic) (ha : ¬IsUnit a) (hap : a ∣ p) :

theorem Polynomial.natDegree_pos_of_not_isUnit_of_dvd_monic {R : Type u} [CommSemiring R] {a p : Polynomial R} (hp : p.Monic) (ha : ¬IsUnit a) (hap : a ∣ p) :

0 < a.natDegree