From ce84116168710ef8c2d80fe7334494f2f0fd2f4d Mon Sep 17 00:00:00 2001
From: Quang Dao <quang.dao@layerzerolabs.org>
Date: Wed, 25 Feb 2026 16:43:07 -0800
Subject: [PATCH] =?UTF-8?q?Implement=20eval=E2=82=82Hom,=20isEmptyRingEqui?=
 =?UTF-8?q?v,=20and=20SMulZeroClass=20for=20CMvPolynomial?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

- eval₂Hom: computable RingHom with toFun := eval₂, proofs via eval₂_equiv
- isEmptyRingEquiv: CMvPolynomial 0 R ≃+* R via isEmptyAlgEquiv
- SMulZeroClass: scalar multiplication r • p = C r * p

Removes the previous sorry-based SMulZeroClass stub from CMvPolynomial.lean.

Made-with: Cursor
---
 CompPoly/Multivariate/CMvPolynomial.lean | 12 +--------
 CompPoly/Multivariate/MvPolyEquiv.lean   | 34 ++++++++++++++++++++++++
 2 files changed, 35 insertions(+), 11 deletions(-)

diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean
index dc0010e..7b7e14a 100644
--- a/CompPoly/Multivariate/CMvPolynomial.lean
+++ b/CompPoly/Multivariate/CMvPolynomial.lean
@@ -259,15 +259,6 @@ def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
 
 -- `renameEquiv` is defined in `CompPoly.Multivariate.Rename`
 
-/-- Scalar multiplication with zero handling.
-
-  This is automatically provided by `Module`, but we list it for completeness.
-
-  TODO: Requires `Module` instance (see above).
--/
-instance {n : ℕ} {R : Type} [Zero R] [BEq R] [LawfulBEq R] : SMulZeroClass R (CMvPolynomial n R) :=
-  sorry
-
 /-- `CMvPolynomial n R` forms a commutative ring when `R` is a commutative ring.
 
   Extends the `CommSemiring` structure with subtraction.
@@ -317,9 +308,8 @@ end CMvPolynomial
 --       (circular dependency):
 -- TODO: `Algebra R (CMvPolynomial n R)` instance
 -- TODO: `Module R (CMvPolynomial n R)` instance
--- TODO: `eval₂Hom` - Ring homomorphism for evaluation
 -- TODO: `finSuccEquiv` - Equivalence between (n+1)-variable and n-variable polynomials
 -- TODO: `optionEquivLeft` - Equivalence for option-indexed variables
--- TODO: `isEmptyAlgEquiv` - Algebra equivalence for empty variable set
+-- See MvPolyEquiv.lean for: eval₂Hom, isEmptyRingEquiv, SMulZeroClass
 
 end CPoly
diff --git a/CompPoly/Multivariate/MvPolyEquiv.lean b/CompPoly/Multivariate/MvPolyEquiv.lean
index b152485..4eb6e43 100644
--- a/CompPoly/Multivariate/MvPolyEquiv.lean
+++ b/CompPoly/Multivariate/MvPolyEquiv.lean
@@ -6,6 +6,7 @@ Authors: Frantisek Silvasi, Julian Sutherland, Andrei Burdușa
 import Batteries.Data.Vector.Lemmas
 import CompPoly.Multivariate.CMvPolynomial
 import Mathlib.Algebra.MvPolynomial.Basic
+import Mathlib.Algebra.MvPolynomial.Equiv
 import Mathlib.Algebra.Ring.Defs
 import CompPoly.Multivariate.Lawful
 import Batteries.Data.Vector.Basic
@@ -463,4 +464,37 @@ lemma degreeOf_equiv {S : Type} {p : CMvPolynomial n R} [CommSemiring S] :
 
 end
 
+namespace CMvPolynomial
+
+variable {n : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
+
+/-- `eval₂` as a ring homomorphism. -/
+def eval₂Hom {S : Type} [CommSemiring S]
+    (f : R →+* S) (vs : Fin n → S) : CMvPolynomial n R →+* S where
+  toFun := eval₂ f vs
+  map_zero' := by simp [eval₂_equiv]
+  map_one' := by simp [eval₂_equiv]
+  map_add' _ _ := by simp [eval₂_equiv, MvPolynomial.eval₂_add]
+  map_mul' _ _ := by simp [eval₂_equiv, MvPolynomial.eval₂_mul]
+
+@[simp]
+lemma eval₂Hom_apply {S : Type} [CommSemiring S]
+    (f : R →+* S) (vs : Fin n → S) (p : CMvPolynomial n R) :
+    eval₂Hom f vs p = eval₂ f vs p := rfl
+
+/-- Ring equivalence between `CMvPolynomial 0 R` and `R`. -/
+noncomputable def isEmptyRingEquiv : CMvPolynomial 0 R ≃+* R :=
+  polyRingEquiv.trans (MvPolynomial.isEmptyAlgEquiv R (Fin 0)).toRingEquiv
+
+instance instSMul : SMul R (CMvPolynomial n R) where
+  smul r p := C r * p
+
+instance instSMulZeroClass : SMulZeroClass R (CMvPolynomial n R) where
+  smul_zero r := mul_zero (C r)
+
+@[simp]
+lemma smul_def (r : R) (p : CMvPolynomial n R) : r • p = C r * p := rfl
+
+end CMvPolynomial
+
 end CPoly