[Merged by Bors] - chore(Algebra/Polynomial/Degree): split Definitions.lean

Mathlib.lean

@@ -760,8 +760,14 @@ import Mathlib.Algebra.Polynomial.Cardinal
 import Mathlib.Algebra.Polynomial.Coeff
 import Mathlib.Algebra.Polynomial.Degree.CardPowDegree
 import Mathlib.Algebra.Polynomial.Degree.Definitions
+import Mathlib.Algebra.Polynomial.Degree.Domain
 import Mathlib.Algebra.Polynomial.Degree.Lemmas
+import Mathlib.Algebra.Polynomial.Degree.Monomial
+import Mathlib.Algebra.Polynomial.Degree.Operations
+import Mathlib.Algebra.Polynomial.Degree.SmallDegree
+import Mathlib.Algebra.Polynomial.Degree.Support
 import Mathlib.Algebra.Polynomial.Degree.TrailingDegree
+import Mathlib.Algebra.Polynomial.Degree.Units
 import Mathlib.Algebra.Polynomial.DenomsClearable
 import Mathlib.Algebra.Polynomial.Derivation
 import Mathlib.Algebra.Polynomial.Derivative

Mathlib/Algebra/Polynomial/CancelLeads.lean

@@ -3,7 +3,6 @@ Copyright (c) 2020 Aaron Anderson. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Aaron Anderson
 -/
-import Mathlib.Algebra.Polynomial.Degree.Definitions
 import Mathlib.Algebra.Polynomial.Degree.Lemmas
 import Mathlib.Tactic.ComputeDegree
 

Mathlib/Algebra/Polynomial/Degree/Domain.lean

@@ -0,0 +1,95 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
+-/
+import Mathlib.Algebra.Polynomial.Degree.Operations
+
+/-!
+# 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
+-/
+
+noncomputable section
+
+open Finsupp Finset
+
+open Polynomial
+
+namespace Polynomial
+
+universe u v
+
+variable {R : Type u} {S : Type v} {a b c d : R} {n m : ℕ}
+
+section Semiring
+
+variable [Semiring R] [NoZeroDivisors R] {p q : R[X]}
+
+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]
+
+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]
+
+@[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
+
+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 _ _
+
+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
+
+lemma eq_zero_of_dvd_of_degree_lt (h₁ : p ∣ q) (h₂ : degree q < degree p) : q = 0 := by
+  by_contra hc
+  exact (lt_iff_not_ge _ _).mp h₂ (degree_le_of_dvd h₁ hc)
+
+lemma eq_zero_of_dvd_of_natDegree_lt (h₁ : p ∣ q) (h₂ : natDegree q < natDegree p) :
+    q = 0 := by
+  by_contra hc
+  exact (lt_iff_not_ge _ _).mp h₂ (natDegree_le_of_dvd h₁ hc)
+
+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)
+
+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)
+
+/-- 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]
+
+end Semiring
+
+section Ring
+
+variable [Ring R] [Nontrivial R] [IsDomain R] {p q : R[X]}
+
+instance : IsDomain R[X] := NoZeroDivisors.to_isDomain _
+
+end Ring
+end Polynomial

Mathlib/Algebra/Polynomial/Degree/Monomial.lean

@@ -0,0 +1,46 @@
+/-
+Copyright (c) 2018 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes, Johannes Hölzl, Kim Morrison, Jens Wagemaker
+-/
+import Mathlib.Algebra.Polynomial.Degree.Definitions
+import Mathlib.Algebra.Polynomial.Monomial
+import Mathlib.Data.Nat.SuccPred
+
+/-!
+# Degree of univariate monomials
+-/
+
+noncomputable section
+
+open Finsupp Finset Polynomial
+
+namespace Polynomial
+
+universe u v
+
+variable {R : Type u} {S : Type v} {a b c d : R} {n m : ℕ}
+
+section Semiring
+
+variable [Semiring R] {p q : R[X]} {ι : Type*}
+
+lemma natDegree_le_pred (hf : p.natDegree ≤ n) (hn : p.coeff n = 0) : p.natDegree ≤ n - 1 := by
+  obtain _ | n := n
+  · exact hf
+  · refine (Nat.le_succ_iff_eq_or_le.1 hf).resolve_left fun h ↦ ?_
+    rw [← Nat.succ_eq_add_one, ← h, coeff_natDegree, leadingCoeff_eq_zero] at hn
+    aesop
+
+theorem monomial_natDegree_leadingCoeff_eq_self (h : #p.support ≤ 1) :
+    monomial p.natDegree p.leadingCoeff = p := by
+  classical
+  rcases card_support_le_one_iff_monomial.1 h with ⟨n, a, rfl⟩
+  by_cases ha : a = 0 <;> simp [ha]
+
+theorem C_mul_X_pow_eq_self (h : #p.support ≤ 1) : C p.leadingCoeff * X ^ p.natDegree = p := by
+  rw [C_mul_X_pow_eq_monomial, monomial_natDegree_leadingCoeff_eq_self h]
+
+end Semiring
+
+end Polynomial