Documentation

Mathlib.Algebra.Polynomial.Degree.Units

Degree of polynomials that are units #

source
theorem Polynomial.natDegree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} (h : IsUnit p) :
p.natDegree = 0
source
theorem Polynomial.degree_eq_zero_of_isUnit {R : Type u} [Semiring R] [NoZeroDivisors R] {p : Polynomial R} [Nontrivial R] (h : IsUnit p) :
p.degree = 0
source
@[simp]
theorem Polynomial.degree_coe_units {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) :
(↑u).degree = 0
source
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.

source
theorem Polynomial.not_isUnit_of_degree_pos {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < p.degree) :
¬IsUnit p
source
theorem Polynomial.not_isUnit_of_natDegree_pos {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (hpl : 0 < p.natDegree) :
¬IsUnit p
source
@[simp]
theorem Polynomial.natDegree_coe_units {R : Type u} [Semiring R] [NoZeroDivisors R] (u : (Polynomial R)ˣ) :
(↑u).natDegree = 0
source
theorem Polynomial.coeff_coe_units_zero_ne_zero {R : Type u} [Semiring R] [NoZeroDivisors R] [Nontrivial R] (u : (Polynomial R)ˣ) :
(↑u).coeff 0 ≠ 0
source
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
source
theorem Polynomial.Monic.degree_pos_of_not_isUnit {R : Type u} [CommSemiring R] {p : Polynomial R} (hp : p.Monic) (hu : ¬IsUnit p) :
0 < p.degree
source
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
source
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) :
0 < a.degree
source
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