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

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} [Semiring R] (p : Polynomial R) {S : Type u_1} [Semiring S] [IsDomain S] [Module S R] [Module.IsTorsionFree S R] {a : S} (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.