Implement CommRing instance for CMvPolynomial

[eliasjudin]

This PR adds proofs autoformalised by @Aristotle-Harmonic.

It moves the transfer lemmas and ring-structure instances needed for CMvPolynomial into CompPoly/Multivariate/CMvPolynomial.lean and updates CompPoly/Multivariate/MvPolyEquiv.lean to reuse those declarations. This resolves the circular dependency blocker and implements CommRing (CMvPolynomial n R)
Closes #55.

Co-authored-by: Aristotle (Harmonic) aristotle-harmonic@harmonic.fun

[github-actions]

🤖 Gemini PR Summary

Implements the CommRing instance for computable multivariate polynomials (CMvPolynomial), completing the formal algebraic specification and eliminating remaining sorry placeholders.

Mathematical Formalization

• Ring Instances: Establishes CommSemiring and CommRing instances for CMvPolynomial.
• Transfer Strategy: Utilizes fromCMvPolynomial to create an injection into Mathlib’s MvPolynomial. This allows algebraic properties to be transferred from the standard library to the computable representation rather than proving axioms from scratch.
• Verification: Replaces auto-formalized placeholders with complete proofs, ensuring CMvPolynomial is a fully verified representation of the commutative ring $R[X_1, \dots, X_n]$.

Infrastructure & Dependency Management

• Circular Dependency Resolution: Moves the definition of fromCMvPolynomial, its morphism proofs, and algebraic instances from MvPolyEquiv.lean to CMvPolynomial.lean.
• Refactoring: Updates MvPolyEquiv.lean to consume centralized declarations from CMvPolynomial.lean, resulting in a linear dependency graph and cleaner proof namespaces (e.g., for degreeOf_equiv).
• Code Quality: Achieves full implementation without introducing new axioms or technical debt.

Impact

Transitions CMvPolynomial from a structural data type to a first-class algebraic object. The implementation allows computable multivariate polynomials to be used in any Lean context requiring CommRing instances, with full compatibility with Mathlib’s standard polynomial library.

---

Analysis of Changes

Metric	Count
📝 Files Changed	2
✅ Lines Added	352
❌ Lines Removed	325

---

Lean Declarations

✏️ **Removed:** 12 declaration(s)

• lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma coeff_eq {m} (a : CMvPolynomial n R) : in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma map_add (a b : CMvPolynomial n R) : in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma map_zero : fromCMvPolynomial (0 : CMvPolynomial n R) = 0 in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma fromCMvPolynomial_injective : Function.Injective (@fromCMvPolynomial n R _) in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma coeff_sum [AddCommMonoid α] in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma map_one : fromCMvPolynomial (1 : CMvPolynomial n R) = 1 in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma foldl_eq_sum {β : Type} [AddCommMonoid β] in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma eq_iff_fromCMvPolynomial {u v: CMvPolynomial n R} : in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma map_mul (a b : CMvPolynomial n R) : in CompPoly/Multivariate/MvPolyEquiv.lean
• lemma toList_pairs_monomial_coeff {β : Type} [AddCommMonoid β] in CompPoly/Multivariate/MvPolyEquiv.lean
• def fromCMvPolynomial (p : CMvPolynomial n R) : MvPolynomial (Fin n) R in CompPoly/Multivariate/MvPolyEquiv.lean

✏️ **Added:** 20 declaration(s)

• lemma map_add (a b : CMvPolynomial n R) : in CompPoly/Multivariate/CMvPolynomial.lean
• lemma fromCMvPolynomial_injective : Function.Injective (@fromCMvPolynomial n R _) in CompPoly/Multivariate/CMvPolynomial.lean
• instance instAddCommMonoid {n : ℕ} : AddCommMonoid (CPoly.CMvPolynomial n R) where in CompPoly/Multivariate/CMvPolynomial.lean
• instance instAddCommSemigroup {n : ℕ} : AddCommSemigroup (CPoly.CMvPolynomial n R) where in CompPoly/Multivariate/CMvPolynomial.lean
• lemma coeff_sum [AddCommMonoid α] in CompPoly/Multivariate/CMvPolynomial.lean
• lemma map_one : fromCMvPolynomial (1 : CMvPolynomial n R) = 1 in CompPoly/Multivariate/CMvPolynomial.lean
• lemma foldl_eq_sum {β : Type} [AddCommMonoid β] in CompPoly/Multivariate/CMvPolynomial.lean
• lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial in CompPoly/Multivariate/CMvPolynomial.lean
• instance instMonoidWithZero {n : ℕ} : MonoidWithZero (CPoly.CMvPolynomial n R) where in CompPoly/Multivariate/CMvPolynomial.lean
• instance instCommRing {n : ℕ} : CommRing (CMvPolynomial n R) where in CompPoly/Multivariate/CMvPolynomial.lean
• lemma map_mul (a b : CMvPolynomial n R) : in CompPoly/Multivariate/CMvPolynomial.lean
• lemma toList_pairs_monomial_coeff {β : Type} [AddCommMonoid β] in CompPoly/Multivariate/CMvPolynomial.lean
• instance instSemiring {n : ℕ} : Semiring (CPoly.CMvPolynomial n R) where in CompPoly/Multivariate/CMvPolynomial.lean
• lemma coeff_eq {m} (a : CMvPolynomial n R) : in CompPoly/Multivariate/CMvPolynomial.lean
• instance instCommSemiring {n : ℕ} : CommSemiring (CPoly.CMvPolynomial n R) where in CompPoly/Multivariate/CMvPolynomial.lean
• def fromCMvPolynomial (p : CMvPolynomial n R) : MvPolynomial (Fin n) R in CompPoly/Multivariate/CMvPolynomial.lean
• instance instAddMonoid {n : ℕ} : AddMonoid (CPoly.CMvPolynomial n R) where in CompPoly/Multivariate/CMvPolynomial.lean
• lemma eq_iff_fromCMvPolynomial {u v : CMvPolynomial n R} : in CompPoly/Multivariate/CMvPolynomial.lean
• lemma map_zero : fromCMvPolynomial (0 : CMvPolynomial n R) = 0 in CompPoly/Multivariate/CMvPolynomial.lean
• lemma map_neg (a : CMvPolynomial n R) : in CompPoly/Multivariate/CMvPolynomial.lean

---

sorry Tracking

✅ **Removed:** 1 `sorry`(s)

• instance {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] : in CompPoly/Multivariate/CMvPolynomial.lean

---

🎨 **Style Guide Adherence**

The following violations of the style guide were identified:

• Line 153: lemma degreeOf_equiv {S : Type} ... uses S and R for type variables. Quote: "Variable Conventions: α, β, γ, ... : Generic types".
• Line 153: lemma degreeOf_equiv is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 268: variable {n : ℕ} {R : Type} uses R for a type variable. Quote: "Variable Conventions: α, β, γ, ... : Generic types".
• Line 274: ... := by grind has by on the same line as the tactic. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 275: Empty line inside the definition fromCMvPolynomial. Quote: "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 278: lemma coeff_eq is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 282: lemma eq_iff_fromCMvPolynomial is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 285: ... := by is on the same line as the statement. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 293: lemma fromCMvPolynomial_injective is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 293: ... := by has by on the same line as the statement. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 297: lemma map_add is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 300: ... := by has by on the same line as the statement. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 342: lemma map_zero is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 342: ... := by has by on the same line as the statement. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 359: fun x y => uses => instead of ↦. Quote: "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 362: lemma map_one is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 362: ... := by has by on the same line as the statement. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 368: Empty line inside the proof of map_one. Quote: "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 378: Empty line inside the proof of map_one. Quote: "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 389: Empty line inside the proof of map_one. Quote: "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 399: Empty line inside the proof of map_one. Quote: "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 415: add_assoc := by aesop ... has by on the same line as the tactic. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 416: add_comm := by grind has by on the same line as the tactic. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 419: zero_add _ := by aesop has by on the same line as the tactic. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 420: add_zero _ := by aesop has by on the same line as the tactic. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 422: nsmul_succ := by grind has by on the same line as the tactic. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 426: add_comm := by grind has by on the same line as the tactic. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 429: lemma toList_pairs_monomial_coeff is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 429: fun term => uses => instead of ↦. Quote: "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 431: fun m => uses => instead of ↦. Quote: "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 432: ... := by has by on the same line as the statement. Quote: "Tactic Mode: Place by at the end of the line preceding the tactic block."
• Line 433: Empty line inside the proof of toList_pairs_monomial_coeff. Quote: "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 441: lemma foldl_eq_sum is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 448: fun x m c => uses => instead of ↦. Quote: "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 459: lemma coeff_sum is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 470: lemma fromCMvPolynomial_sum_eq_sum_fromCMvPolynomial is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 478: lemma map_mul is missing a docstring. Quote: "Every definition and major theorem should have a docstring."
• Line 566: variable {n : ℕ} {R : Type} uses R for a type variable. Quote: "Variable Conventions: α, β, γ, ... : Generic types".
• Line 568: lemma map_neg is missing a docstring. Quote: "Every definition and major theorem should have a docstring."

---

📄 **Per-File Summaries**

• CompPoly/Multivariate/CMvPolynomial.lean: This change introduces the fromCMvPolynomial injection to Mathlib's MvPolynomial and leverages it to provide fully proved CommSemiring and CommRing instances for computable multivariate polynomials, replacing previous placeholder implementations with a transfer-based proof strategy.
• CompPoly/Multivariate/MvPolyEquiv.lean: This change refactors CompPoly/Multivariate/MvPolyEquiv.lean by removing the definition of fromCMvPolynomial and its associated algebraic morphism proofs and semiring instances, while refining the proof of degreeOf_equiv for better namespace clarity.

---

Last updated: 2026-03-03 10:15 UTC.