From 559f6bd0b01d6bd6807129d06aab8a1a382c7496 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Sat, 14 Feb 2026 13:11:00 -0600
Subject: [PATCH 01/15] added typeclass instances and definitions for degreeLE
 and degreeLT

---
 CompPoly/Univariate/Basic.lean | 43 ++++++++++++++++++++++++++++++++++
 1 file changed, 43 insertions(+)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index be5a63a..1da43ab 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -533,6 +533,16 @@ lemma pow_succ_right [Nontrivial R]
         convert Raw.mul_assoc p ( p ^ n ) p using 1;
         grind
 
+/--
+`CPolynomial R` forms a commutative monoid when `R` is a semiring.
+-/
+instance : AddCommMonoid (CPolynomial R) where
+  zero_add := zero_add
+  add_zero := by intro p; exact add_zero p
+  nsmul := nsmul
+  nsmul_zero := nsmul_zero
+  nsmul_succ := nsmul_succ
+
 /-- `CPolynomial R` forms a semiring when `R` is a semiring.
 
   The semiring structure extends the `AddCommGroup` structure with multiplication.
@@ -778,6 +788,39 @@ instance : Mod (CPolynomial R) := ⟨mod⟩
 
 end Division
 
+section ModuleTheory
+
+-- The assumptions are requried for `CPolynomial R` to be a module and s0 are necessary downsteam.
+variable [Semiring R] [LawfulBEq R]
+
+--TODO: Fill sorries state theorems.
+
+/-- `CPolynomail` forms a module when R is a semiring. -/
+instance : Module R (CPolynomial R) where
+  smul:= sorry
+  mul_smul := sorry
+  one_smul := sorry --likely requires non-trivial R
+  smul_zero := sorry
+  smul_add := sorry
+  add_smul := sorry
+  zero_smul := sorry
+
+/-- This is an R-linear function that returns the cofficient of X^n. -/
+def lcoeff (n : ℕ) : (CPolynomial R) →ₗ[R] R where
+  toFun p := coeff p n
+  map_add' p q := coeff_add p q n
+  map_smul' r p := sorry --coeff_smul r p n
+
+/-- The `R`-submodule of `CPolynomial R` consisting of polynomials of degree ≤ `n`. -/
+def degreeLE (n : WithBot ℕ) : Submodule R (CPolynomial R) :=
+  ⨅ k : ℕ, ⨅ _ : ↑k > n, LinearMap.ker (lcoeff k)
+
+/-- The `R`-submodule of `CPolynomial R` consisting of polynomials of degree < `n`. -/
+def degreeLT (n : ℕ) : Submodule R (CPolynomial R) :=
+  ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff k)
+
+end ModuleTheory
+
 end CPolynomial
 
 end CompPoly

From a107fc8995b3da3a7ecf18c427c2a1556a1c3544 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Sat, 14 Feb 2026 14:10:25 -0600
Subject: [PATCH 02/15] Filled in sorries for typeclass instance

---
 CompPoly/Univariate/Basic.lean | 66 +++++++++++++++++++++++++++++-----
 1 file changed, 57 insertions(+), 9 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 1da43ab..0057588 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -793,23 +793,71 @@ section ModuleTheory
 -- The assumptions are requried for `CPolynomial R` to be a module and s0 are necessary downsteam.
 variable [Semiring R] [LawfulBEq R]
 
---TODO: Fill sorries state theorems.
+/-- Scalar multiplication for canonical polynomials: multiply each coefficient by `r`,
+then trim to restore canonicity. -/
+instance smul : SMul R (CPolynomial R) where
+  smul r p := ⟨(Raw.smul r p.val).trim, Trim.trim_twice _⟩
+
+/-- Coefficient of a scalar multiple. -/
+lemma coeff_smul (r : R) (p : CPolynomial R) (i : ℕ) :
+    coeff (r • p) i = r * coeff p i := by
+  show (Raw.smul r p.val).trim.coeff i = r * p.val.coeff i
+  rw [Trim.coeff_eq_coeff, Raw.smul_equiv]
+
+lemma smul_zero' (r : R) : r • (0 : CPolynomial R) = 0 := by
+  rw [eq_iff_coeff]; intro i
+  rw [coeff_smul, coeff_zero]; simp
+
+lemma smul_eq_of_coeff_eq {p q : CPolynomial R}
+    (h : Trim.equiv p.val q.val) : p = q := by
+  apply CPolynomial.ext
+  exact Trim.canonical_ext p.prop q.prop h
+
+lemma smul_add' (r : R) (p q : CPolynomial R) :
+    r • (p + q) = r • p + r • q := by
+  apply smul_eq_of_coeff_eq; intro i
+  show (Raw.smul r (p.val + q.val)).trim.coeff i =
+    ((Raw.smul r p.val).trim + (Raw.smul r q.val).trim).coeff i
+  rw [Trim.coeff_eq_coeff, smul_equiv, add_coeff_trimmed,
+      add_coeff_trimmed, Trim.coeff_eq_coeff, Trim.coeff_eq_coeff,
+      smul_equiv, smul_equiv]
+  exact Distrib.left_distrib r (p.val.coeff i) (q.val.coeff i)
+
+lemma add_smul' (r s : R) (p : CPolynomial R) :
+    (r + s) • p = r • p + s • p := by
+  rw [eq_iff_coeff]; intro i
+  rw [coeff_smul, coeff_add, coeff_smul, coeff_smul]; grind
+
+lemma zero_smul' (p : CPolynomial R) : (0 : R) • p = 0 := by
+  apply smul_eq_of_coeff_eq; intro i
+  show (Raw.smul 0 p.val).trim.coeff i = (0 : Raw R).coeff i
+  rw [Trim.coeff_eq_coeff, smul_equiv]
+  exact MulZeroClass.zero_mul (p.val.coeff i)
+
+lemma one_smul' (p : CPolynomial R) : (1 : R) • p = p := by
+  rw [eq_iff_coeff]; intro i
+  rw [coeff_smul, _root_.one_mul]
+
+lemma mul_smul' (r s : R) (p : CPolynomial R) :
+    (r * s) • p = r • (s • p) := by
+  rw [eq_iff_coeff]; intro i
+  rw [coeff_smul, coeff_smul, coeff_smul, _root_.mul_assoc]
 
 /-- `CPolynomail` forms a module when R is a semiring. -/
 instance : Module R (CPolynomial R) where
-  smul:= sorry
-  mul_smul := sorry
-  one_smul := sorry --likely requires non-trivial R
-  smul_zero := sorry
-  smul_add := sorry
-  add_smul := sorry
-  zero_smul := sorry
+  smul:= SMul.smul
+  mul_smul := mul_smul'
+  one_smul := one_smul'
+  smul_zero := smul_zero'
+  smul_add := smul_add'
+  add_smul := add_smul'
+  zero_smul := zero_smul'
 
 /-- This is an R-linear function that returns the cofficient of X^n. -/
 def lcoeff (n : ℕ) : (CPolynomial R) →ₗ[R] R where
   toFun p := coeff p n
   map_add' p q := coeff_add p q n
-  map_smul' r p := sorry --coeff_smul r p n
+  map_smul' r p := coeff_smul r p n
 
 /-- The `R`-submodule of `CPolynomial R` consisting of polynomials of degree ≤ `n`. -/
 def degreeLE (n : WithBot ℕ) : Submodule R (CPolynomial R) :=

From 09102b840b1c093dfba00d60c1c5b990036ed0c3 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Sat, 14 Feb 2026 14:28:59 -0600
Subject: [PATCH 03/15] added theorem statements.

---
 CompPoly/Univariate/Basic.lean | 22 ++++++++++++++++++++--
 1 file changed, 20 insertions(+), 2 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 0057588..ccb842f 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -860,13 +860,31 @@ def lcoeff (n : ℕ) : (CPolynomial R) →ₗ[R] R where
   map_smul' r p := coeff_smul r p n
 
 /-- The `R`-submodule of `CPolynomial R` consisting of polynomials of degree ≤ `n`. -/
-def degreeLE (n : WithBot ℕ) : Submodule R (CPolynomial R) :=
+def degreeLE (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : WithBot ℕ) :
+    Submodule S (CPolynomial S) :=
   ⨅ k : ℕ, ⨅ _ : ↑k > n, LinearMap.ker (lcoeff k)
 
 /-- The `R`-submodule of `CPolynomial R` consisting of polynomials of degree < `n`. -/
-def degreeLT (n : ℕ) : Submodule R (CPolynomial R) :=
+def degreeLT (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) :
+    Submodule S (CPolynomial S) :=
   ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff k)
 
+theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R n ↔ degree p ≤ n := by
+    sorry
+
+theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) : degreeLE R m ≤ degreeLE R n := fun _ hf =>
+  mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
+
+-- TODO add version of degreeLE_eq_span_X_pow and degreeLT_eq_span_X_pow
+
+theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degree p < n := by
+  sorry
+
+theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
+  mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h_lessThan)
+
+
+--TOOD Add linear equivalance
 end ModuleTheory
 
 end CPolynomial

From 853728319b9dfb79325b8ae7f5aa130e2b5020d0 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Sat, 14 Feb 2026 14:33:00 -0600
Subject: [PATCH 04/15] fixed linter issue

---
 CompPoly/Univariate/Basic.lean | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index ccb842f..805c3d8 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -790,7 +790,7 @@ end Division
 
 section ModuleTheory
 
--- The assumptions are requried for `CPolynomial R` to be a module and s0 are necessary downsteam.
+-- The assumptions are requried for `CPolynomial R` to be a module and s0 are necessary downstream.
 variable [Semiring R] [LawfulBEq R]
 
 /-- Scalar multiplication for canonical polynomials: multiply each coefficient by `r`,
@@ -872,7 +872,8 @@ def degreeLT (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) :
 theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R n ↔ degree p ≤ n := by
     sorry
 
-theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) : degreeLE R m ≤ degreeLE R n := fun _ hf =>
+theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
+   degreeLE R m ≤ degreeLE R n := fun _ hf =>
   mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
 
 -- TODO add version of degreeLE_eq_span_X_pow and degreeLT_eq_span_X_pow
@@ -883,8 +884,8 @@ theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degr
 theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
   mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h_lessThan)
 
-
 --TOOD Add linear equivalance
+
 end ModuleTheory
 
 end CPolynomial

From ddd6f992a42020f1603e1718e2ab7b252188c7be Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Sat, 14 Feb 2026 14:34:13 -0600
Subject: [PATCH 05/15] fixing linter issue

---
 CompPoly/Univariate/Basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 805c3d8..59aa032 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -873,8 +873,8 @@ theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R
     sorry
 
 theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
-   degreeLE R m ≤ degreeLE R n := fun _ hf =>
-  mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
+    degreeLE R m ≤ degreeLE R n := fun _ hf =>
+        mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
 
 -- TODO add version of degreeLE_eq_span_X_pow and degreeLT_eq_span_X_pow
 

From 186d26904e26a6ec516d9efbff2ab748fbf84928 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Sun, 15 Feb 2026 18:32:10 -0600
Subject: [PATCH 06/15] Update Basic.lean

Filled in sorries
---
 CompPoly/Univariate/Basic.lean | 98 ++++++++++++++++++++++++++++++++--
 1 file changed, 95 insertions(+), 3 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 59aa032..2f815b4 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -869,8 +869,98 @@ def degreeLT (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) :
     Submodule S (CPolynomial S) :=
   ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff k)
 
+/-- A polynomial has degree ≤ n iff all coefficients at indices > n are zero. -/
+theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ) :
+    p.degree ≤ n ↔ ∀ k : ℕ, n < k → p.coeff k = 0 := by
+      constructor
+      · intro hn k hk
+        contrapose! hn
+        refine' lt_of_lt_of_le hk _
+        unfold CPolynomial.degree
+        unfold CPolynomial.Raw.degree
+        cases h : p.val.lastNonzero <;> simp_all +decide;
+        · have := p.prop;
+          unfold CPolynomial.Raw.trim at this; aesop;
+        · have h_coeff_zero : ∀ i, i >
+              (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                  → p.val.coeff i = 0 := by
+            intro i hi;
+            have h_coeff_zero : ∀ i, i >
+                (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                    → p.val.coeff i = 0 := by
+              intro i hi
+              have h_lastNonzero : ∀ j, j >
+                  (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                      → p.val.coeff j = 0 := by
+                intro j hj
+                have h_lastNonzero : ∀ j, j >
+                    (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                        → p.val.coeff j = 0 := by
+                  intro j hj
+                  have h_lastNonzero : ∀ j, j >
+                      (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                          → p.val.coeff j = 0 := by
+                    intro j hj
+                    exact (by
+                      have := p.prop
+                      replace this := congr_arg ( fun q => q.coeff j ) this
+                      simp_all +decide [ CPolynomial.Raw.trim ]
+                      rw [ ← this, Array.getElem?_eq_none ] <;> aesop)
+                  exact h_lastNonzero j hj
+                exact h_lastNonzero j hj
+              exact h_lastNonzero i hi
+            exact h_coeff_zero i hi;
+          exact le_of_not_gt fun hk' => hn <| by simpa using h_coeff_zero k hk'
+      · cases' eq_or_ne p ( 0 : CompPoly.CPolynomial R )
+            with hp hp <;> simp_all +decide [ CompPoly.CPolynomial.coeff ]
+        · simp [CompPoly.CPolynomial.degree]
+          simp +decide [ CompPoly.CPolynomial.Raw.degree ]
+          cases n <;> simp +decide [ CompPoly.CPolynomial.Raw.lastNonzero ]
+          · simp +decide [ Array.findIdxRev? ]
+            unfold Array.findIdxRev?.find; aesop
+          · cases h : Array.findIdxRev? ( fun x => x != 0 ) ( 0 : Array R ) <;> simp_all +decide
+            cases ‹Fin _› ; contradiction
+        · intro h
+          contrapose! h
+          obtain ⟨ k, hk ⟩ := degree_eq_support_max p hp
+          unfold CompPoly.CPolynomial.support at hk; aesop
+
+theorem degree_lt_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : ℕ) :
+    p.degree < n ↔ ∀ k : ℕ, n ≤ k → p.coeff k = 0 := by
+    match n with
+    | 0 =>
+        have h_deg_lt_zero : p.degree < 0 → p = 0 := by
+          intro h_deg_neg
+          have h_zero : p = 0 := by
+            contrapose! h_deg_neg
+            obtain ⟨ k, hk ⟩ := degree_eq_support_max p h_deg_neg
+            exact hk.2.symm ▸ Nat.cast_nonneg _
+          exact h_zero
+        apply Iff.intro
+        · intro h k; induction k <;> simp_all +decide
+          · rfl
+          · (expose_names; exact h_1)
+        · intro h; exact (by
+          convert degree_le_iff_coeff_zero p ⊥ using 1;
+          simp +decide [ h ])
+    | m+1 =>
+        have nat_ineq : p.degree < ((m + 1) : ℕ) ↔ p.degree ≤ m := by
+          refine CovBy.lt_iff_le_left ?_
+          have : m < m+1 := by omega
+          constructor
+          · exact WithBot.coe_lt_coe.mpr (by omega)
+          · intro c hc1 hc2
+            rcases c with _ | c
+            · exact absurd hc1 (not_lt.mpr bot_le)
+            · exact absurd hc2 (not_lt_of_ge (Order.succ_le_of_lt hc1))
+        norm_cast at nat_ineq
+        rw [nat_ineq]
+        have nat_ineq_2 ( k : ℕ ): m+1 ≤ k ↔ m < k := by omega
+        simpa using degree_le_iff_coeff_zero p m
+
 theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R n ↔ degree p ≤ n := by
-    sorry
+    simp [degreeLE]
+    exact Iff.symm (degree_le_iff_coeff_zero p n)
 
 theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
     degreeLE R m ≤ degreeLE R n := fun _ hf =>
@@ -879,12 +969,14 @@ theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
 -- TODO add version of degreeLE_eq_span_X_pow and degreeLT_eq_span_X_pow
 
 theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degree p < n := by
-  sorry
+    simp [degreeLT]
+    rw[degree_lt_iff_coeff_zero]
+    exact Lex.forall
 
 theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
   mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h_lessThan)
 
---TOOD Add linear equivalance
+-- TODO: add linear equivalence.
 
 end ModuleTheory
 

From 111691e646152018a64b2de8dc7b2cd9833b88e3 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Sun, 15 Feb 2026 18:34:09 -0600
Subject: [PATCH 07/15] fixed linter issue

---
 CompPoly/Univariate/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 2f815b4..36b0a81 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -919,7 +919,7 @@ theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ)
           · simp +decide [ Array.findIdxRev? ]
             unfold Array.findIdxRev?.find; aesop
           · cases h : Array.findIdxRev? ( fun x => x != 0 ) ( 0 : Array R ) <;> simp_all +decide
-            cases ‹Fin _› ; contradiction
+            cases ‹Fin _›; contradiction
         · intro h
           contrapose! h
           obtain ⟨ k, hk ⟩ := degree_eq_support_max p hp

From 109f593469422d5ec6b2a205d54ad89f31fa706c Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Mon, 16 Feb 2026 17:58:54 -0600
Subject: [PATCH 08/15] Update Basic.lean

Cleaned up some notational fluff from Aristotle.
---
 CompPoly/Univariate/Basic.lean | 22 ++++++++++------------
 1 file changed, 10 insertions(+), 12 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 36b0a81..8ea520a 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -882,23 +882,23 @@ theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ)
         · have := p.prop;
           unfold CPolynomial.Raw.trim at this; aesop;
         · have h_coeff_zero : ∀ i, i >
-              (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+              (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
                   → p.val.coeff i = 0 := by
             intro i hi;
             have h_coeff_zero : ∀ i, i >
-                (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
                     → p.val.coeff i = 0 := by
               intro i hi
               have h_lastNonzero : ∀ j, j >
-                  (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                  (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
                       → p.val.coeff j = 0 := by
                 intro j hj
                 have h_lastNonzero : ∀ j, j >
-                    (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                    (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
                         → p.val.coeff j = 0 := by
                   intro j hj
                   have h_lastNonzero : ∀ j, j >
-                      (↑‹Fin (Array.size (↑p : CompPoly.CPolynomial.Raw R))› : ℕ)
+                      (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
                           → p.val.coeff j = 0 := by
                     intro j hj
                     exact (by
@@ -912,10 +912,10 @@ theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ)
             exact h_coeff_zero i hi;
           exact le_of_not_gt fun hk' => hn <| by simpa using h_coeff_zero k hk'
       · cases' eq_or_ne p ( 0 : CompPoly.CPolynomial R )
-            with hp hp <;> simp_all +decide [ CompPoly.CPolynomial.coeff ]
-        · simp [CompPoly.CPolynomial.degree]
-          simp +decide [ CompPoly.CPolynomial.Raw.degree ]
-          cases n <;> simp +decide [ CompPoly.CPolynomial.Raw.lastNonzero ]
+            with hp hp <;> simp_all +decide [ coeff ]
+        · simp [degree]
+          simp +decide [ CPolynomial.Raw.degree ]
+          cases n <;> simp +decide [ CPolynomial.Raw.lastNonzero ]
           · simp +decide [ Array.findIdxRev? ]
             unfold Array.findIdxRev?.find; aesop
           · cases h : Array.findIdxRev? ( fun x => x != 0 ) ( 0 : Array R ) <;> simp_all +decide
@@ -923,7 +923,7 @@ theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ)
         · intro h
           contrapose! h
           obtain ⟨ k, hk ⟩ := degree_eq_support_max p hp
-          unfold CompPoly.CPolynomial.support at hk; aesop
+          unfold support at hk; aesop
 
 theorem degree_lt_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : ℕ) :
     p.degree < n ↔ ∀ k : ℕ, n ≤ k → p.coeff k = 0 := by
@@ -976,8 +976,6 @@ theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degr
 theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
   mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h_lessThan)
 
--- TODO: add linear equivalence.
-
 end ModuleTheory
 
 end CPolynomial

From 32c0ab8cf926e0848bd08cdc23af94fc453f196c Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Thu, 19 Feb 2026 12:02:01 -0600
Subject: [PATCH 09/15] Doc strings and one new theorem added

---
 CompPoly/Univariate/Basic.lean | 25 ++++++++++++++++++++++---
 1 file changed, 22 insertions(+), 3 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 8ea520a..e1b9ee8 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -790,7 +790,7 @@ end Division
 
 section ModuleTheory
 
--- The assumptions are requried for `CPolynomial R` to be a module and s0 are necessary downstream.
+-- The assumptions are requried for `CPolynomial R` to be a module and so are necessary downstream.
 variable [Semiring R] [LawfulBEq R]
 
 /-- Scalar multiplication for canonical polynomials: multiply each coefficient by `r`,
@@ -804,15 +804,18 @@ lemma coeff_smul (r : R) (p : CPolynomial R) (i : ℕ) :
   show (Raw.smul r p.val).trim.coeff i = r * p.val.coeff i
   rw [Trim.coeff_eq_coeff, Raw.smul_equiv]
 
+/-- Scalar multiplication on 0 gives 0. -/
 lemma smul_zero' (r : R) : r • (0 : CPolynomial R) = 0 := by
   rw [eq_iff_coeff]; intro i
   rw [coeff_smul, coeff_zero]; simp
 
+/-- Two CPolynomials are equal if the underlying Raw CPolynomials are trim equivalent. -/
 lemma smul_eq_of_coeff_eq {p q : CPolynomial R}
     (h : Trim.equiv p.val q.val) : p = q := by
   apply CPolynomial.ext
   exact Trim.canonical_ext p.prop q.prop h
 
+/-- Scalar multiplication distributes. -/
 lemma smul_add' (r : R) (p q : CPolynomial R) :
     r • (p + q) = r • p + r • q := by
   apply smul_eq_of_coeff_eq; intro i
@@ -823,21 +826,25 @@ lemma smul_add' (r : R) (p q : CPolynomial R) :
       smul_equiv, smul_equiv]
   exact Distrib.left_distrib r (p.val.coeff i) (q.val.coeff i)
 
+/-- Scalar multiplication distributes across scalar addition. -/
 lemma add_smul' (r s : R) (p : CPolynomial R) :
     (r + s) • p = r • p + s • p := by
   rw [eq_iff_coeff]; intro i
   rw [coeff_smul, coeff_add, coeff_smul, coeff_smul]; grind
 
+/-- Scalar multiplication by 0 gives 0. -/
 lemma zero_smul' (p : CPolynomial R) : (0 : R) • p = 0 := by
   apply smul_eq_of_coeff_eq; intro i
   show (Raw.smul 0 p.val).trim.coeff i = (0 : Raw R).coeff i
   rw [Trim.coeff_eq_coeff, smul_equiv]
   exact MulZeroClass.zero_mul (p.val.coeff i)
 
+/-- Scalar multiplication on p by 1 gives p. -/
 lemma one_smul' (p : CPolynomial R) : (1 : R) • p = p := by
   rw [eq_iff_coeff]; intro i
   rw [coeff_smul, _root_.one_mul]
 
+/-- Scalar multiplication is associative. -/
 lemma mul_smul' (r s : R) (p : CPolynomial R) :
     (r * s) • p = r • (s • p) := by
   rw [eq_iff_coeff]; intro i
@@ -925,6 +932,8 @@ theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ)
           obtain ⟨ k, hk ⟩ := degree_eq_support_max p hp
           unfold support at hk; aesop
 
+/-- A polynomial has degree less than `n` iff the coefficients of X^k are zero for k
+    greater than `n`. -/
 theorem degree_lt_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : ℕ) :
     p.degree < n ↔ ∀ k : ℕ, n ≤ k → p.coeff k = 0 := by
     match n with
@@ -958,24 +967,34 @@ theorem degree_lt_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : ℕ) :
         have nat_ineq_2 ( k : ℕ ): m+1 ≤ k ↔ m < k := by omega
         simpa using degree_le_iff_coeff_zero p m
 
+/-- A polynomial is contained in `degreeLE R n` iff if has degree at most `n`. -/
 theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R n ↔ degree p ≤ n := by
     simp [degreeLE]
     exact Iff.symm (degree_le_iff_coeff_zero p n)
 
+/-- The submodule of polynomials with degree less than or equal to `n ` contains the submodule
+  of polynomials with degree less or equal to than `m` when `m` is less than or equal to `n`. -/
 theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
     degreeLE R m ≤ degreeLE R n := fun _ hf =>
         mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
 
--- TODO add version of degreeLE_eq_span_X_pow and degreeLT_eq_span_X_pow
-
+/-- A polynomial is contained in `degreeLT R n` iff if has degree less than `n`. -/
 theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degree p < n := by
     simp [degreeLT]
     rw[degree_lt_iff_coeff_zero]
     exact Lex.forall
 
+/-- The submodule of polynomials with degree strictly less than `n ` contains the submodule
+  of polynomials with degree at less than `m` when `m` is less than or equal to `n`. -/
 theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
   mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h_lessThan)
 
+/-- The submodule of polynomials with degree strictly less than `n + 1` equals the submodule
+  of polynomials with degree at most `n`. -/
+theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R ↑n := by
+  simp +decide [ degreeLT, degreeLE ]
+  rfl
+
 end ModuleTheory
 
 end CPolynomial

From 5ae512de85b6d623beb8bce1c3631cd258e602ab Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Thu, 19 Feb 2026 13:04:41 -0600
Subject: [PATCH 10/15] added theorems about bases of degreeLT and degreeLE

---
 CompPoly/Univariate/Basic.lean | 112 +++++++++++++++++++++++++++++++--
 1 file changed, 106 insertions(+), 6 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index e1b9ee8..cc68979 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -809,7 +809,8 @@ lemma smul_zero' (r : R) : r • (0 : CPolynomial R) = 0 := by
   rw [eq_iff_coeff]; intro i
   rw [coeff_smul, coeff_zero]; simp
 
-/-- Two CPolynomials are equal if the underlying Raw CPolynomials are trim equivalent. -/
+/-- Helper lemma: Two CPolynomials are equal if
+    the underlying Raw CPolynomials are trim equivalent. -/
 lemma smul_eq_of_coeff_eq {p q : CPolynomial R}
     (h : Trim.equiv p.val q.val) : p = q := by
   apply CPolynomial.ext
@@ -877,7 +878,7 @@ def degreeLT (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] (n : ℕ) :
   ⨅ k : ℕ, ⨅ (_ : k ≥ n), LinearMap.ker (lcoeff k)
 
 /-- A polynomial has degree ≤ n iff all coefficients at indices > n are zero. -/
-theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ) :
+theorem degree_le_iff_coeff_zero (p : CPolynomial R) (n : WithBot ℕ) :
     p.degree ≤ n ↔ ∀ k : ℕ, n < k → p.coeff k = 0 := by
       constructor
       · intro hn k hk
@@ -918,7 +919,7 @@ theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ)
               exact h_lastNonzero i hi
             exact h_coeff_zero i hi;
           exact le_of_not_gt fun hk' => hn <| by simpa using h_coeff_zero k hk'
-      · cases' eq_or_ne p ( 0 : CompPoly.CPolynomial R )
+      · cases' eq_or_ne p ( 0 : CPolynomial R )
             with hp hp <;> simp_all +decide [ coeff ]
         · simp [degree]
           simp +decide [ CPolynomial.Raw.degree ]
@@ -934,7 +935,7 @@ theorem degree_le_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : WithBot ℕ)
 
 /-- A polynomial has degree less than `n` iff the coefficients of X^k are zero for k
     greater than `n`. -/
-theorem degree_lt_iff_coeff_zero (p : CompPoly.CPolynomial R) (n : ℕ) :
+theorem degree_lt_iff_coeff_zero (p : CPolynomial R) (n : ℕ) :
     p.degree < n ↔ ∀ k : ℕ, n ≤ k → p.coeff k = 0 := by
     match n with
     | 0 =>
@@ -973,7 +974,7 @@ theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R
     exact Iff.symm (degree_le_iff_coeff_zero p n)
 
 /-- The submodule of polynomials with degree less than or equal to `n ` contains the submodule
-  of polynomials with degree less or equal to than `m` when `m` is less than or equal to `n`. -/
+    of polynomials with degree less or equal to than `m` when `m` is less than or equal to `n`. -/
 theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
     degreeLE R m ≤ degreeLE R n := fun _ hf =>
         mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
@@ -985,7 +986,7 @@ theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degr
     exact Lex.forall
 
 /-- The submodule of polynomials with degree strictly less than `n ` contains the submodule
-  of polynomials with degree at less than `m` when `m` is less than or equal to `n`. -/
+    of polynomials with degree at less than `m` when `m` is less than or equal to `n`. -/
 theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
   mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h_lessThan)
 
@@ -995,6 +996,105 @@ theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R 
   simp +decide [ degreeLT, degreeLE ]
   rfl
 
+/-- When `R` has decidable equality so does `(CPolynomial R)`. -/
+instance [DecidableEq R] : DecidableEq (CPolynomial R) :=
+  inferInstanceAs (DecidableEq { p : CPolynomial.Raw R // p.trim = p })
+
+section bases
+
+-- This section contains theorems and lemmas about generators of submodules of `CPolynomial R`.
+
+/-- Helper lemma: The degree of `monomial n c` is `n`. -/
+lemma degree_monomial [DecidableEq R] (n : ℕ) (c : R) (hc : c ≠ 0) :
+  degree (monomial n c) = n := by
+    have := degree_eq_support_max ( monomial n c )
+    specialize this (by
+    unfold monomial
+    simp +decide [ Raw.monomial, hc ]
+    erw [ Subtype.mk_eq_mk ]; simp +decide [ Raw.mk ])
+    obtain ⟨ k, hk, hk' ⟩ := this; simp_all +decide [ support ]
+    unfold monomial at *; simp_all +decide
+    unfold CPolynomial.Raw.monomial at *; simp_all +decide
+    grind
+
+/--  Helper lemma: `monomial n r` is equal to `X^n` times `r`.-/
+lemma monomial_eq_smul_X_pow [DecidableEq R] [Nontrivial R] (n : ℕ) (r : R) :
+  monomial n r = r • ((X : CPolynomial R) ^ n) := by
+    have h_smul : r • (X ^ n : CPolynomial R)
+        = (C r : CPolynomial R) * (X ^ n : CPolynomial R) := by
+      have h_coeff : ∀ (p : CPolynomial R) (i : ℕ), coeff (r • p) i
+          = coeff (C r * p) i := by
+        intro p i; rw [ coeff_smul, coeff_mul ]; simp +decide [ Finset.sum_range_succ' ]
+        rw [ Finset.sum_eq_zero ] <;> simp +decide
+        · have h_coeff_C : (C r).val.coeff 0 = r := by
+            exact coeff_C r 0 |> Eq.trans <| if_pos rfl
+          generalize_proofs at *; (
+          cases h : ( C r : CPolynomial.Raw R ); aesop;)
+        · intro x hx; rcases x with ( _ | x ) <;> simp +decide [ C ]
+          · rw [ CPolynomial.Raw.trim ]; aesop
+          · unfold CPolynomial.Raw.trim; aesop
+      generalize_proofs at *; (
+      exact eq_iff_coeff.2 fun i => h_coeff _ _ ▸ rfl)
+    exact h_smul.symm ▸ (C_mul_X_pow_eq_monomial r n).symm
+
+/-- Helper lemma: We can write a monomial as a sum of monomials multiplied by the coefficients. -/
+lemma eq_sum_monomials [DecidableEq R] (p : CPolynomial R) :
+  p = (Finset.range (p.natDegree + 1)).sum (fun i => .monomial i (coeff p i)) := by
+    rw [eq_iff_coeff]; intro i
+    have h_distrib : coeff (∑ j ∈ Finset.range (p.natDegree + 1),
+        monomial j (coeff p j)) i =
+      ∑ j ∈ Finset.range (p.natDegree + 1), coeff (monomial j (coeff p j)) i := by
+      change (lcoeff i) (∑ j ∈ _, _) = ∑ j ∈ _, (lcoeff i) _
+      exact map_sum _ _ _
+    rw [h_distrib]
+    simp only [coeff_monomial]
+    by_cases hi : i ≤ p.natDegree
+    · rw [Finset.sum_eq_single_of_mem i
+        (Finset.mem_range.mpr (by omega))
+        (fun j _ hji => if_neg (fun h => hji h.symm))]
+      simp
+    · push_neg at hi
+      have h_coeff_zero : coeff p i = 0 := by
+        by_cases hp : p = 0
+        · aesop
+        · exact (degree_lt_iff_coeff_zero p i).mp
+            (by rw [degree_eq_natDegree p hp]; exact_mod_cast hi) i le_rfl
+      rw [h_coeff_zero]; symm
+      exact Finset.sum_eq_zero fun j hj => by
+        exact if_neg (by have := Finset.mem_range.mp hj; omega)
+
+/-- `degreeLE R ↑n` is spanned by monic monomials of degree at most `n`. -/
+theorem degreeLE_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} :
+  degreeLE R ↑n =
+    Submodule.span R ↑((Finset.range (n + 1)).image fun n => (X : CPolynomial R) ^ n) := by
+  symm
+  refine' le_antisymm _ _ <;> intro p hp <;> simp_all +decide [ degreeLE ]
+  · refine' Submodule.span_induction _ _ _ _ hp
+    · rintro _ ⟨ i, hi, rfl ⟩ j hj
+      have h_coeff_zero : (X ^ i : CPolynomial R).coeff j = 0 := by
+        have h_coeff_zero : (X ^ i : CPolynomial R).coeff j = if j = i then 1 else 0 := by
+          have h_coeff_zero : (X ^ i : CPolynomial R) = monomial i 1 := by
+            rw [ monomial_eq_smul_X_pow ]
+            exact Eq.symm (one_smul' (X ^ i))
+          rw [ h_coeff_zero, coeff_monomial ]
+        rw [ h_coeff_zero, if_neg ( by linarith [ Set.mem_Iio.mp hi ] ) ]
+      exact h_coeff_zero
+    · aesop
+    · aesop
+    · aesop
+  · have h_sum_monomials : p = Finset.sum (Finset.range (p.natDegree + 1))
+         (fun i => (p.coeff i) • (X : CPolynomial R) ^ i) := by
+      convert eq_sum_monomials p using 1
+      exact Finset.sum_congr rfl fun i hi => by rw [ monomial_eq_smul_X_pow ]
+    rw [ h_sum_monomials ]
+    refine' Submodule.sum_mem _ _
+    intro i hi
+    by_cases h : i ≤ n
+    · exact Submodule.smul_mem _ _ ( Submodule.subset_span ⟨ i, Nat.lt_succ_of_le h, rfl ⟩ )
+    · simp +decide [ show p.coeff i = 0 from hp i ( not_le.mp h ) ] at hi ⊢
+
+end bases
+
 end ModuleTheory
 
 end CPolynomial

From 6c3b48ab13be678a8fb83fd8500a9e3828a55341 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Thu, 19 Feb 2026 14:08:34 -0600
Subject: [PATCH 11/15] Added the linear equivalence between degreeLT R n and
 R^n

---
 CompPoly/Univariate/Basic.lean | 173 +++++++++++++++++++++++++++++++--
 1 file changed, 164 insertions(+), 9 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index cc68979..f14672f 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -472,6 +472,17 @@ theorem degree_eq_natDegree (p : CPolynomial R) (hp : p ≠ 0) :
   unfold natDegree Raw.natDegree
   rw [hk]
 
+omit [LawfulBEq R] in
+/-- Lemma for computing the degree of 0 in proofs. -/
+lemma degree_zero : degree (0 : CPolynomial R) = ⊥ := by
+  unfold degree Raw.degree
+  have : (0 : CPolynomial.Raw R).lastNonzero = none := by
+    simp [Raw.lastNonzero]
+    apply Array.findIdxRev?_empty_none
+    rfl
+  show Raw.degree (0 : CPolynomial.Raw R) = ⊥
+  rw [Raw.degree, this]
+
 end Operations
 
 section Semiring
@@ -790,7 +801,8 @@ end Division
 
 section ModuleTheory
 
--- The assumptions are requried for `CPolynomial R` to be a module and so are necessary downstream.
+-- The assumptions are requried for `CPolynomial R` to be a module and are necessary downstream.
+
 variable [Semiring R] [LawfulBEq R]
 
 /-- Scalar multiplication for canonical polynomials: multiply each coefficient by `r`,
@@ -996,17 +1008,17 @@ theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R 
   simp +decide [ degreeLT, degreeLE ]
   rfl
 
-/-- When `R` has decidable equality so does `(CPolynomial R)`. -/
-instance [DecidableEq R] : DecidableEq (CPolynomial R) :=
-  inferInstanceAs (DecidableEq { p : CPolynomial.Raw R // p.trim = p })
-
 section bases
 
 -- This section contains theorems and lemmas about generators of submodules of `CPolynomial R`.
 
+/-- When `R` has decidable equality so does `(CPolynomial R)`. -/
+instance [DecidableEq R] : DecidableEq (CPolynomial R) :=
+  inferInstanceAs (DecidableEq { p : CPolynomial.Raw R // p.trim = p })
+
 /-- Helper lemma: The degree of `monomial n c` is `n`. -/
 lemma degree_monomial [DecidableEq R] (n : ℕ) (c : R) (hc : c ≠ 0) :
-  degree (monomial n c) = n := by
+    degree (monomial n c) = n := by
     have := degree_eq_support_max ( monomial n c )
     specialize this (by
     unfold monomial
@@ -1019,7 +1031,7 @@ lemma degree_monomial [DecidableEq R] (n : ℕ) (c : R) (hc : c ≠ 0) :
 
 /--  Helper lemma: `monomial n r` is equal to `X^n` times `r`.-/
 lemma monomial_eq_smul_X_pow [DecidableEq R] [Nontrivial R] (n : ℕ) (r : R) :
-  monomial n r = r • ((X : CPolynomial R) ^ n) := by
+    monomial n r = r • ((X : CPolynomial R) ^ n) := by
     have h_smul : r • (X ^ n : CPolynomial R)
         = (C r : CPolynomial R) * (X ^ n : CPolynomial R) := by
       have h_coeff : ∀ (p : CPolynomial R) (i : ℕ), coeff (r • p) i
@@ -1039,7 +1051,7 @@ lemma monomial_eq_smul_X_pow [DecidableEq R] [Nontrivial R] (n : ℕ) (r : R) :
 
 /-- Helper lemma: We can write a monomial as a sum of monomials multiplied by the coefficients. -/
 lemma eq_sum_monomials [DecidableEq R] (p : CPolynomial R) :
-  p = (Finset.range (p.natDegree + 1)).sum (fun i => .monomial i (coeff p i)) := by
+    p = (Finset.range (p.natDegree + 1)).sum (fun i => .monomial i (coeff p i)) := by
     rw [eq_iff_coeff]; intro i
     have h_distrib : coeff (∑ j ∈ Finset.range (p.natDegree + 1),
         monomial j (coeff p j)) i =
@@ -1065,7 +1077,7 @@ lemma eq_sum_monomials [DecidableEq R] (p : CPolynomial R) :
 
 /-- `degreeLE R ↑n` is spanned by monic monomials of degree at most `n`. -/
 theorem degreeLE_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} :
-  degreeLE R ↑n =
+    degreeLE R ↑n =
     Submodule.span R ↑((Finset.range (n + 1)).image fun n => (X : CPolynomial R) ^ n) := by
   symm
   refine' le_antisymm _ _ <;> intro p hp <;> simp_all +decide [ degreeLE ]
@@ -1093,8 +1105,151 @@ theorem degreeLE_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} :
     · exact Submodule.smul_mem _ _ ( Submodule.subset_span ⟨ i, Nat.lt_succ_of_le h, rfl ⟩ )
     · simp +decide [ show p.coeff i = 0 from hp i ( not_le.mp h ) ] at hi ⊢
 
+/-- `degreeLT R ↑n` is spanned by monic monomials of degree less than `n`. -/
+theorem degreeLT_eq_span_X_pow [DecidableEq R] [Nontrivial R] {n : ℕ} :
+    degreeLT R n
+        = Submodule.span R ↑((Finset.range n).image fun n => (X : CPolynomial R) ^ n) := by
+      cases n with
+    | zero =>
+      simp only [Finset.range_zero, Finset.image_empty, Finset.coe_empty, Submodule.span_empty]
+      ext p; simp [Submodule.mem_bot, mem_degreeLT, eq_zero_iff_coeff_zero]
+      have zero : (∀ (i : ℕ), (p.val : Array R)[i]?.getD 0 = 0) ↔ p = 0 := by
+        rw [eq_iff_coeff]; simp
+        exact⟨fun h i => (h i).trans (coeff_zero i).symm, fun h i => (h i).trans
+  (coeff_zero i)⟩
+      have zero_deg : p.degree = ⊥ ↔ p = 0 := by
+        constructor
+        · intro h
+          have hlt : p.degree < ↑(0 : ℕ) := by rw [h]; exact WithBot.bot_lt_coe 0
+          exact eq_zero_iff_coeff_zero.mpr
+            (fun k => (degree_lt_iff_coeff_zero p 0).mp hlt k (Nat.zero_le k))
+        · rintro rfl; exact degree_zero
+      rw [zero_deg]
+      grind
+    | succ m => rw [degreeLT_succ_eq_degreeLE, degreeLE_eq_span_X_pow]
+
 end bases
 
+section LinearEquivalences
+
+-- This section contains theorem about lienar isomoprhism between modules.
+
+/-- The sum `∑ i : Fin n, monomial i (f i)` has degree less than `n`,
+  so it lies in `degreeLT R n`. -/
+lemma degreeLTEquiv_invFun_mem [DecidableEq R] (n : ℕ) (f : Fin n → R) :
+    Finset.univ.sum (fun i : Fin n => monomial (↑i) (f i)) ∈ degreeLT R n := by
+  simp [degreeLT]
+  intro i hi
+  simp [lcoeff, monomial]
+  rw [ Finset.sum_eq_zero ]; intros; simp_all +decide [ CPolynomial.Raw.monomial ];
+  grind
+
+/-- The forward map of `degreeLTEquiv` preserves addition:
+  extracting coefficients commutes with polynomial addition.  -/
+lemma degreeLTEquiv_map_add (n : ℕ)
+    (p q : ↥(degreeLT R n)) :
+    (fun i : Fin n => coeff (↑(p + q) : CPolynomial R) (↑i)) =
+    (fun i : Fin n => coeff (↑p : CPolynomial R) (↑i) + coeff (↑q : CPolynomial R) (↑i)) := by
+  exact funext fun i => coeff_add _ _ _
+
+/-- The forward map of `degreeLTEquiv` preserves scalar multiplication:
+  extracting coefficients commutes with scalar multiplication. -/
+lemma degreeLTEquiv_map_smul (n : ℕ)
+    (r : R) (p : ↥(degreeLT R n)) :
+    (fun i : Fin n => coeff (↑(r • p) : CPolynomial R) (↑i)) =
+    (fun i : Fin n => r * coeff (↑p : CPolynomial R) (↑i)) := by
+  have h_coeff_smul : ∀ i : ℕ, coeff (r • (p : CPolynomial R)) i
+      = r *coeff (p : CPolynomial R) i := by
+    exact fun i => coeff_smul r (↑p) i
+  exact funext fun i => h_coeff_smul i
+
+/-- Left inverse: reconstructing a polynomial from its coefficients via monomials
+  recovers the original polynomial. -/
+lemma degreeLTEquiv_left_inv [DecidableEq R] (n : ℕ)
+    (p : ↥(degreeLT R n)) :
+    (⟨Finset.univ.sum (fun i : Fin n => monomial (↑i) (coeff p.1 i)),
+      degreeLTEquiv_invFun_mem n (fun i => coeff p.1 i)⟩ : ↥(degreeLT R n)) = p := by
+    apply Subtype.ext
+    rw [eq_iff_coeff]; intro i
+    rw [show coeff (∑ j : Fin n, monomial (↑j) (coeff p.1 j)) i =
+      ∑ j : Fin n, coeff (monomial (↑j) (coeff p.1 j)) i from map_sum (lcoeff i) _ _]
+    simp only [coeff_monomial]
+    by_cases hi : i < n
+    · rw [Finset.sum_eq_single_of_mem ⟨i, hi⟩ (Finset.mem_univ _)
+        (fun j _ hji => if_neg fun h => hji (Fin.ext (by aesop)))]
+      simp
+    · rw [show coeff p.1 i = 0 from
+        (degree_lt_iff_coeff_zero p.1 n).mp (mem_degreeLT.mp p.2) i (by omega)]
+      exact Finset.sum_eq_zero fun j _ => if_neg (by have := j.isLt; omega)
+
+/-- Right inverse: extracting coefficients from the polynomial built from `f`
+  recovers `f`. -/
+lemma degreeLTEquiv_right_inv [DecidableEq R] (n : ℕ)
+    (f : Fin n → R) :
+    (fun i : Fin n => coeff
+      (Finset.univ.sum (fun j : Fin n => monomial (↑j) (f j))) i) = f := by
+    funext i
+    rw [show coeff (∑ j : Fin n, monomial (↑j) (f j)) ↑i =
+      ∑ j : Fin n, coeff (monomial (↑j) (f j)) ↑i from map_sum (lcoeff ↑i) _ _]
+    simp only [coeff_monomial]
+    rw [Finset.sum_eq_single_of_mem i (Finset.mem_univ _)
+      (fun j _ hji => if_neg fun h => hji (Fin.ext (by omega)))]
+    simp
+
+/-- The first `n` coefficients on `degreeLT n` form a linear equivalence with `Fin n → R`.
+
+  This is the computable polynomial analogue of `Polynomial.degreeLTEquiv`.
+
+  The forward map sends a polynomial `p` with `degree p < n` to the function
+  `i ↦ coeff p i` for `i : Fin n`.
+
+  The inverse map sends a function `f : Fin n → R` to the polynomial
+  `∑ i, monomial i (f i)`. -/
+def degreeLTEquiv (S : Type*) [BEq S] [Semiring S] [LawfulBEq S] [DecidableEq S] (n : ℕ) :
+    degreeLT S n ≃ₗ[S] (Fin n → S) where
+  toFun p i := coeff p.1 i
+  invFun f :=
+    ⟨Finset.univ.sum (fun i : Fin n => monomial (↑i) (f i)),
+      by exact degreeLTEquiv_invFun_mem n f⟩
+  map_add' := fun p q => degreeLTEquiv_map_add n p q
+  map_smul' := fun r p => degreeLTEquiv_map_smul n r p
+  left_inv := by apply degreeLTEquiv_left_inv
+  right_inv := by intro f; generalize_proofs at *; exact degreeLTEquiv_right_inv n f
+
+/-- The `degreeLTEquiv` maps a polynomial to zero if and only if the polynomial is zero. -/
+theorem degreeLTEquiv_eq_zero_iff_eq_zero [DecidableEq R] {n : ℕ} {p : CPolynomial R}
+    (hp : p ∈ degreeLT R n) :
+    degreeLTEquiv R n ⟨p, hp⟩ = 0 ↔ p = 0 := by simp
+
+/-- Evaluation of a polynomial in `degreeLT R n` can be expressed as a sum over its
+  coefficients via `degreeLTEquiv`. -/
+theorem eval_eq_sum_degreeLTEquiv [DecidableEq R] {n : ℕ} {p : CPolynomial R}
+    (hp : p ∈ degreeLT R n) (x : R) :
+    eval x p =
+      Finset.univ.sum (fun i : Fin n => degreeLTEquiv R n ⟨p, hp⟩ i * x ^ (i : ℕ)) := by
+  unfold CPolynomial.eval degreeLTEquiv;
+  unfold CPolynomial.Raw.eval; simp +decide
+  have h_coeff_zero : ∀ i ≥ n, p.val.coeff i = 0 := by
+    intro i hi; have := hp; simp_all +decide [ degreeLT ]
+    convert hp i hi using 1
+    unfold CPolynomial.lcoeff; aesop
+  have h_sum_eq : ∑ i ∈ Finset.range (p.val.size), (p.val.coeff i) * x ^ i
+      = ∑ i ∈ Finset.range n, (p.val.coeff i) * x ^ i := by
+    by_cases h : n ≤ p.val.size <;> simp_all +decide
+    · rw [ ← Finset.sum_range_add_sum_Ico _ h ]
+      simp +decide [ Finset.sum_Ico_eq_sum_range, h_coeff_zero ]
+    · rw [ Finset.sum_subset ( Finset.range_mono h.le ) fun i hi₁ hi₂ => by aesop ]
+  convert h_sum_eq using 1
+  · unfold CPolynomial.Raw.eval₂
+    induction' ( p.val : Array R ) using Array.recOn with p ih; simp +decide
+    induction p using List.reverseRecOn <;> simp +decide [ *, Finset.sum_range_succ ]
+    simp_all +decide [ List.zipIdx_append ]
+    exact congr_arg₂ _ ( Finset.sum_congr rfl fun i hi => by
+         rw [ List.getElem?_append ]; aesop ) rfl
+  · simp +decide [ Finset.sum_range, CPolynomial.Raw.coeff ]
+
+end LinearEquivalences
+
 end ModuleTheory
 
 end CPolynomial

From c2b3318eab48171987e46215d125f098e9a8c883 Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Thu, 19 Feb 2026 14:24:19 -0600
Subject: [PATCH 12/15] Fixed typos in docstrings.

---
 CompPoly/Univariate/Basic.lean | 18 +++++++++---------
 1 file changed, 9 insertions(+), 9 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index f14672f..7fb274b 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -801,7 +801,7 @@ end Division
 
 section ModuleTheory
 
--- The assumptions are requried for `CPolynomial R` to be a module and are necessary downstream.
+-- The assumptions are required for `CPolynomial R` to be a module and are necessary downstream.
 
 variable [Semiring R] [LawfulBEq R]
 
@@ -863,7 +863,7 @@ lemma mul_smul' (r s : R) (p : CPolynomial R) :
   rw [eq_iff_coeff]; intro i
   rw [coeff_smul, coeff_smul, coeff_smul, _root_.mul_assoc]
 
-/-- `CPolynomail` forms a module when R is a semiring. -/
+/-- `CPolynomial` forms a module when R is a semiring. -/
 instance : Module R (CPolynomial R) where
   smul:= SMul.smul
   mul_smul := mul_smul'
@@ -873,7 +873,7 @@ instance : Module R (CPolynomial R) where
   add_smul := add_smul'
   zero_smul := zero_smul'
 
-/-- This is an R-linear function that returns the cofficient of X^n. -/
+/-- This is an R-linear function that returns the coefficient of X^n. -/
 def lcoeff (n : ℕ) : (CPolynomial R) →ₗ[R] R where
   toFun p := coeff p n
   map_add' p q := coeff_add p q n
@@ -980,25 +980,25 @@ theorem degree_lt_iff_coeff_zero (p : CPolynomial R) (n : ℕ) :
         have nat_ineq_2 ( k : ℕ ): m+1 ≤ k ↔ m < k := by omega
         simpa using degree_le_iff_coeff_zero p m
 
-/-- A polynomial is contained in `degreeLE R n` iff if has degree at most `n`. -/
+/-- A polynomial is contained in `degreeLE R n` iff it has degree at most `n`. -/
 theorem mem_degreeLE {n : WithBot ℕ} {p : (CPolynomial R)} : p ∈ degreeLE R n ↔ degree p ≤ n := by
     simp [degreeLE]
     exact Iff.symm (degree_le_iff_coeff_zero p n)
 
-/-- The submodule of polynomials with degree less than or equal to `n ` contains the submodule
-    of polynomials with degree less or equal to than `m` when `m` is less than or equal to `n`. -/
+/-- The submodule of polynomials with degree less than or equal to `n` contains the submodule
+    of polynomials with degree less than or equal to `m` when `m` is less than or equal to `n`. -/
 theorem degreeLE_mono (m n : WithBot ℕ) (h_lessThan : m ≤ n) :
     degreeLE R m ≤ degreeLE R n := fun _ hf =>
         mem_degreeLE.2 (le_trans (mem_degreeLE.1 hf) h_lessThan)
 
-/-- A polynomial is contained in `degreeLT R n` iff if has degree less than `n`. -/
+/-- A polynomial is contained in `degreeLT R n` iff it has degree less than `n`. -/
 theorem mem_degreeLT {n : ℕ} {p : CPolynomial R} : p ∈ degreeLT R n ↔ degree p < n := by
     simp [degreeLT]
     rw[degree_lt_iff_coeff_zero]
     exact Lex.forall
 
 /-- The submodule of polynomials with degree strictly less than `n ` contains the submodule
-    of polynomials with degree at less than `m` when `m` is less than or equal to `n`. -/
+    of polynomials with degree less than `m` when `m` is less than or equal to `n`. -/
 theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degreeLT R n := fun _ hf =>
   mem_degreeLT.2 (lt_of_lt_of_le (mem_degreeLT.1 hf) <| WithBot.coe_le_coe.2 h_lessThan)
 
@@ -1132,7 +1132,7 @@ end bases
 
 section LinearEquivalences
 
--- This section contains theorem about lienar isomoprhism between modules.
+-- This section contains theorem about linear isomoprhism between modules.
 
 /-- The sum `∑ i : Fin n, monomial i (f i)` has degree less than `n`,
   so it lies in `degreeLT R n`. -/

From df066b8f3105732e9579063fd447dcb1f767c89e Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Thu, 19 Feb 2026 14:34:41 -0600
Subject: [PATCH 13/15] Updated two proofs that claude code Identified as
 likely to cause issues.

---
 CompPoly/Univariate/Basic.lean | 52 +++++++++++-----------------------
 1 file changed, 16 insertions(+), 36 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 7fb274b..db6bfa7 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -707,13 +707,13 @@ lemma monomial_add_erase [DecidableEq R] (p : CPolynomial R) :
     (expose_names; exact inst_1.toSemiring)
     (expose_names; exact inst)
     (expose_names; exact inst_2)
-    exact Raw.monomial p.natDegree p.leadingCoeff;
-    exact p.val - Raw.monomial p.natDegree ( p.val.coeff p.natDegree );
+    exact Raw.monomial p.natDegree p.leadingCoeff
+    exact p.val - Raw.monomial p.natDegree ( p.val.coeff p.natDegree )
     · exact Eq.symm Array.getD_eq_getD_getElem?
-    · convert Eq.symm ( add_sub_cancel _ _ ) using 1;
-      congr! 1;
-      convert Raw.sub_coeff _ _ _ using 1;
-      · congr! 1;
+    · convert Eq.symm ( add_sub_cancel _ _ ) using 1
+      congr! 1
+      convert Raw.sub_coeff _ _ _ using 1
+      · congr! 1
         · exact Eq.symm Array.getD_eq_getD_getElem?
         · congr! 1
           congr! 1
@@ -901,36 +901,16 @@ theorem degree_le_iff_coeff_zero (p : CPolynomial R) (n : WithBot ℕ) :
         cases h : p.val.lastNonzero <;> simp_all +decide;
         · have := p.prop;
           unfold CPolynomial.Raw.trim at this; aesop;
-        · have h_coeff_zero : ∀ i, i >
+        · have h_coeff_zero : ∀ j : ℕ, j >
               (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
-                  → p.val.coeff i = 0 := by
-            intro i hi;
-            have h_coeff_zero : ∀ i, i >
-                (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
-                    → p.val.coeff i = 0 := by
-              intro i hi
-              have h_lastNonzero : ∀ j, j >
-                  (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
-                      → p.val.coeff j = 0 := by
-                intro j hj
-                have h_lastNonzero : ∀ j, j >
-                    (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
-                        → p.val.coeff j = 0 := by
-                  intro j hj
-                  have h_lastNonzero : ∀ j, j >
-                      (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
-                          → p.val.coeff j = 0 := by
-                    intro j hj
-                    exact (by
-                      have := p.prop
-                      replace this := congr_arg ( fun q => q.coeff j ) this
-                      simp_all +decide [ CPolynomial.Raw.trim ]
-                      rw [ ← this, Array.getElem?_eq_none ] <;> aesop)
-                  exact h_lastNonzero j hj
-                exact h_lastNonzero j hj
-              exact h_lastNonzero i hi
-            exact h_coeff_zero i hi;
-          exact le_of_not_gt fun hk' => hn <| by simpa using h_coeff_zero k hk'
+                  → p.val.coeff j = 0 := by
+            intro j hj
+            have htrim := p.prop
+            have := congr_arg (fun q => q.coeff j) htrim
+            simp_all +decide [ CPolynomial.Raw.trim ]
+            rw [ ← this, Array.getElem?_eq_none ] <;> aesop
+          exact le_of_not_gt fun hk' => hn <| by
+            simpa [Raw.coeff, Array.getD_eq_getD_getElem?] using h_coeff_zero k hk'
       · cases' eq_or_ne p ( 0 : CPolynomial R )
             with hp hp <;> simp_all +decide [ coeff ]
         · simp [degree]
@@ -961,7 +941,7 @@ theorem degree_lt_iff_coeff_zero (p : CPolynomial R) (n : ℕ) :
         apply Iff.intro
         · intro h k; induction k <;> simp_all +decide
           · rfl
-          · (expose_names; exact h_1)
+          · assumption
         · intro h; exact (by
           convert degree_le_iff_coeff_zero p ⊥ using 1;
           simp +decide [ h ])

From 4c6346937ce2eed4d3111767491338e76554f95e Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Fri, 20 Feb 2026 09:49:31 -0600
Subject: [PATCH 14/15] typo

---
 CompPoly/Univariate/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index db6bfa7..ca96b47 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -1112,7 +1112,7 @@ end bases
 
 section LinearEquivalences
 
--- This section contains theorem about linear isomoprhism between modules.
+-- This section contains theorems about linear isomorphisms between modules.
 
 /-- The sum `∑ i : Fin n, monomial i (f i)` has degree less than `n`,
   so it lies in `degreeLT R n`. -/

From f50fe5f8fb0f1c7339087932f453c46f4d64ca1f Mon Sep 17 00:00:00 2001
From: Desmond <63413811+desmondcoles1@users.noreply.github.com>
Date: Mon, 23 Feb 2026 18:09:56 -0600
Subject: [PATCH 15/15] fixed error caused by update

after the update a simp + decide term was hitting maximum recursion depth, changing the proof to be more explicit resolved the issue
---
 CompPoly/Univariate/Basic.lean | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/CompPoly/Univariate/Basic.lean b/CompPoly/Univariate/Basic.lean
index 2f671d0..9a983ca 100644
--- a/CompPoly/Univariate/Basic.lean
+++ b/CompPoly/Univariate/Basic.lean
@@ -904,10 +904,10 @@ theorem degree_le_iff_coeff_zero (p : CPolynomial R) (n : WithBot ℕ) :
               (↑‹Fin (Array.size (↑p : CPolynomial.Raw R))› : ℕ)
                   → p.val.coeff j = 0 := by
             intro j hj
-            have htrim := p.prop
-            have := congr_arg (fun q => q.coeff j) htrim
-            simp_all +decide [ CPolynomial.Raw.trim ]
-            rw [ ← this, Array.getElem?_eq_none ] <;> aesop
+            by_cases hjlt : j < p.val.size
+            · rw [Trim.coeff_eq_getElem hjlt]
+              exact (Trim.lastNonzero_spec h).2 j hjlt hj
+            · simp [show p.val.size ≤ j from by omega]
           exact le_of_not_gt fun hk' => hn <| by
             simpa [Raw.coeff, Array.getD_eq_getD_getElem?] using h_coeff_zero k hk'
       · cases' eq_or_ne p ( 0 : CPolynomial R )
@@ -985,7 +985,6 @@ theorem degreeLT_mono {m n : ℕ} (h_lessThan : m ≤ n) : degreeLT R m ≤ degr
   of polynomials with degree at most `n`. -/
 theorem degreeLT_succ_eq_degreeLE {n : ℕ} : degreeLT R (n + 1) = degreeLE R ↑n := by
   simp +decide [ degreeLT, degreeLE ]
-  rfl
 
 section bases