Mathlib.Algebra.Polynomial.Degree.Domain

Polynomial.instNoZeroDivisors instance

: NoZeroDivisors R[X]

Full source

instance : NoZeroDivisors R[X] where
  eq_zero_or_eq_zero_of_mul_eq_zero h := by
    rw [← leadingCoeff_eq_zero, ← leadingCoeff_eq_zero]
    refine eq_zero_or_eq_zero_of_mul_eq_zero ?_
    rw [← leadingCoeff_zero, ← leadingCoeff_mul, h]

Polynomial Ring Preserves No Zero Divisors Property

Informal description

The ring of univariate polynomials $R[X]$ has no zero divisors if the base semiring $R$ has no zero divisors.

Polynomial.natDegree_mul theorem

(hp : p ≠ 0) (hq : q ≠ 0) : (p * q).natDegree = p.natDegree + q.natDegree

Full source

lemma natDegree_mul (hp : p ≠ 0) (hq : q ≠ 0) : (p*q).natDegree = p.natDegree + q.natDegree := by
  rw [← Nat.cast_inj (R := WithBot ℕ), ← degree_eq_natDegree (mul_ne_zero hp hq),
    Nat.cast_add, ← degree_eq_natDegree hp, ← degree_eq_natDegree hq, degree_mul]

Natural Degree of Polynomial Product: $\text{natDegree}(p \cdot q) = \text{natDegree}(p) + \text{natDegree}(q)$

Informal description

For any nonzero polynomials $p$ and $q$ in $R[X]$, the natural degree of their product is the sum of their natural degrees, i.e., $$\text{natDegree}(p \cdot q) = \text{natDegree}(p) + \text{natDegree}(q).$$

Polynomial.natDegree_smul theorem

(ha : a ≠ 0) : (a • p).natDegree = p.natDegree

Full source

lemma natDegree_smul (ha : a ≠ 0) : (a • p).natDegree = p.natDegree := by
  by_cases hp : p = 0
  · simp only [hp, smul_zero]
  · apply natDegree_eq_of_le_of_coeff_ne_zero
    · exact (natDegree_smul_le _ _).trans (le_refl _)
    · simpa only [coeff_smul, coeff_natDegree, smul_eq_mul, ne_eq, mul_eq_zero,
        leadingCoeff_eq_zero, not_or] using ⟨ha, hp⟩

Natural Degree Invariance under Nonzero Scalar Multiplication: $\text{natDegree}(a \cdot p) = \text{natDegree}(p)$ for $a \neq 0$

Informal description

For any nonzero element $a$ in a semiring $R$ and any polynomial $p \in R[X]$, the natural degree of the scalar multiple $a \cdot p$ is equal to the natural degree of $p$, i.e., $\text{natDegree}(a \cdot p) = \text{natDegree}(p)$.

Polynomial.natDegree_pow theorem

(p : R[X]) (n : ℕ) : natDegree (p ^ n) = n * natDegree p

Full source

@[simp]
lemma natDegree_pow (p : R[X]) (n : ℕ) : natDegree (p ^ n) = n * natDegree p := by
  classical
  obtain rfl | hp := eq_or_ne p 0
  · obtain rfl | hn := eq_or_ne n 0 <;> simp [*]
  exact natDegree_pow' <| by
    rw [← leadingCoeff_pow, Ne, leadingCoeff_eq_zero]; exact pow_ne_zero _ hp

Natural Degree of Polynomial Power: $\text{natDegree}(p^n) = n \cdot \text{natDegree}(p)$

Informal description

For any univariate polynomial $p$ over a semiring $R$ and any natural number $n$, the natural degree of $p^n$ is equal to $n$ times the natural degree of $p$, i.e., $$\text{natDegree}(p^n) = n \cdot \text{natDegree}(p).$$

Polynomial.natDegree_le_of_dvd theorem

(h1 : p ∣ q) (h2 : q ≠ 0) : p.natDegree ≤ q.natDegree

Full source

lemma natDegree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : p.natDegree ≤ q.natDegree := by
  obtain ⟨q, rfl⟩ := h1
  rw [mul_ne_zero_iff] at h2
  rw [natDegree_mul h2.1 h2.2]; exact Nat.le_add_right _ _

Natural Degree Inequality for Polynomial Divisibility: $\text{natDegree}(p) \leq \text{natDegree}(q)$ when $p \mid q$ and $q \neq 0$

Informal description

For any univariate polynomials $p$ and $q$ over a semiring $R$, if $p$ divides $q$ and $q$ is nonzero, then the natural degree of $p$ is less than or equal to the natural degree of $q$, i.e., $$\text{natDegree}(p) \leq \text{natDegree}(q).$$

Polynomial.degree_le_of_dvd theorem

(h1 : p ∣ q) (h2 : q ≠ 0) : degree p ≤ degree q

Full source

lemma degree_le_of_dvd (h1 : p ∣ q) (h2 : q ≠ 0) : degree p ≤ degree q := by
  rcases h1 with ⟨q, rfl⟩; rw [mul_ne_zero_iff] at h2
  exact degree_le_mul_left p h2.2

Degree Inequality for Polynomial Divisibility: $\deg(p) \leq \deg(q)$ when $p \mid q$ and $q \neq 0$

Informal description

For any univariate polynomials $p$ and $q$ over a semiring $R$, if $p$ divides $q$ and $q$ is nonzero, then the degree of $p$ is less than or equal to the degree of $q$, i.e., $$\deg(p) \leq \deg(q).$$

Polynomial.not_dvd_of_degree_lt theorem

(h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q

Full source

lemma not_dvd_of_degree_lt (h0 : q ≠ 0) (hl : q.degree < p.degree) : ¬p ∣ q := by
  by_contra hcontra
  exact h0 (eq_zero_of_dvd_of_degree_lt hcontra hl)

Non-divisibility by Higher Degree Polynomials

Informal description

For any nonzero polynomial $q$ and any polynomial $p$, if the degree of $q$ is strictly less than the degree of $p$, then $p$ does not divide $q$.

Polynomial.not_dvd_of_natDegree_lt theorem

(h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) : ¬p ∣ q

Full source

lemma not_dvd_of_natDegree_lt (h0 : q ≠ 0) (hl : q.natDegree < p.natDegree) :
    ¬p ∣ q := by
  by_contra hcontra
  exact h0 (eq_zero_of_dvd_of_natDegree_lt hcontra hl)

Non-divisibility of Polynomials by Higher Degree Polynomials

Informal description

For any nonzero polynomials $p$ and $q$ in $R[X]$, if the natural degree of $q$ is strictly less than that of $p$, then $p$ does not divide $q$.

Polynomial.natDegree_sub_eq_of_prod_eq theorem

 {p₁ p₂ q₁ q₂ : R[X]} (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

Full source

/-- This lemma is useful for working with the `intDegree` of a rational function. -/
lemma natDegree_sub_eq_of_prod_eq {p₁ p₂ q₁ q₂ : R[X]} (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 := by
  rw [sub_eq_sub_iff_add_eq_add]
  norm_cast
  rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]

Degree Difference Equality for Polynomial Products

Informal description

For any nonzero polynomials $p₁, p₂, q₁, q₂ \in R[X]$ such that $p₁ \cdot q₂ = p₂ \cdot q₁$, the difference between the natural degrees of $p₁$ and $q₁$ equals the difference between the natural degrees of $p₂$ and $q₂$, i.e., $$ \text{natDegree}(p₁) - \text{natDegree}(q₁) = \text{natDegree}(p₂) - \text{natDegree}(q₂). $$

Polynomial.instIsDomain instance

: IsDomain R[X]

Full source

instance : IsDomain R[X] := NoZeroDivisors.to_isDomain _

Polynomial Rings over Domains are Domains

Informal description

For any domain $R$, the polynomial ring $R[X]$ is also a domain. That is, $R[X]$ is a nontrivial ring where multiplication by any nonzero polynomial is cancellative on both sides.

Main results