Univariate polynomials form a domain

Main results

• Polynomial.instNoZeroDivisors: R[X] has no zero divisors if R does not
• Polynomial.instDomain: R[X] is a domain if R is

instance Polynomial.instNoZeroDivisors {R : Type u} [Semiring R] [NoZeroDivisors R] : NoZeroDivisors (Polynomial R)

theorem Polynomial.natDegree_mul {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (hp : p ≠ 0) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree

theorem Polynomial.natDegree_smul {R : Type u} {a : R} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (ha : a ≠ 0) : (a • p).natDegree = p.natDegree

@[simp]

theorem Polynomial.natDegree_pow {R : Type u} [Semiring R] [NoZeroDivisors R] (p : Polynomial R) (n : ℕ) : (p ^ n).natDegree = n * p.natDegree

theorem Polynomial.natDegree_le_of_dvd {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h1 : p ∣ q) (h2 : q ≠ 0) : p.natDegree ≤ q.natDegree

theorem Polynomial.degree_le_of_dvd {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h1 : p ∣ q) (h2 : q ≠ 0) : p.degree ≤ q.degree

theorem Polynomial.eq_zero_of_dvd_of_degree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h₁ : p ∣ q) (h₂ : q.degree < p.degree) : q = 0

theorem Polynomial.eq_zero_of_dvd_of_natDegree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h₁ : p ∣ q) (h₂ : q.natDegree < p.natDegree) : q = 0

theorem Polynomial.not_dvd_of_degree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q

theorem Polynomial.not_dvd_of_natDegree_lt {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) : ¬p ∣ q

theorem Polynomial.natDegree_sub_eq_of_prod_eq {R : Type u} [Semiring R] [NoZeroDivisors R] {p₁ p₂ q₁ q₂ : Polynomial R} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0) (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0) (h_eq : p₁ * q₂ = p₂ * q₁) : ↑p₁.natDegree - ↑q₁.natDegree = ↑p₂.natDegree - ↑q₂.natDegree

This lemma is useful for working with the intDegree of a rational function.

instance Polynomial.instIsDomain {R : Type u} [Ring R] [Nontrivial R] [IsDomain R] : IsDomain (Polynomial R)