Documentation

Mathlib.Algebra.Polynomial.Degree.Domain

Univariate polynomials form a domain #

Main results #

theorem Polynomial.degree_le_of_dvd {R : Type u} [Semiring R] [NoZeroDivisors R] {p q : Polynomial R} (h1 : p q) (h2 : q 0) :
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₁) :

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