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