Implement `CommRing` instance for `CMvPolynomial`

[dhsorens]

Implement CommRing instance for CMvPolynomial

Summary

Implement the CommRing instance for CMvPolynomial, extending the CommSemiring structure with subtraction. This is currently blocked by circular dependency issues.

Context

Part of Phase 1: Foundation Completion (API completeness) as outlined in ROADMAP.md line 59. The CommSemiring instance is defined in MvPolyEquiv.lean, but we cannot import it due to circular dependencies.

What to Implement

instance {n : ℕ} {R : Type} [CommRing R] [BEq R] [LawfulBEq R] : CommRing (CMvPolynomial n R)

• Extends the CommSemiring structure with subtraction
• Location: CompPoly/Multivariate/CMvPolynomial.lean lines 253-277
• Currently all fields are sorry due to circular dependency

Dependencies

• CommSemiring instance (defined in MvPolyEquiv.lean, but circular dependency prevents import)
• Neg and Sub operations (need to verify these exist in Lawful.lean)
• All ring axioms (associativity, distributivity, etc.)

Implementation Notes

• Circular Dependency Problem: MvPolyEquiv.lean imports CMvPolynomial.lean, so we cannot import MvPolyEquiv.lean to get the CommSemiring instance
• Potential Solutions:
  1. Move CommSemiring instance to a separate file that both can import
  2. Duplicate the instance definition (not ideal)
  3. Restructure files to break the circular dependency
• Need to verify that Neg and Sub operations exist in Lawful.lean
• Most fields can likely be proven using existing operations, once the dependency is resolved

Fields to Implement

All fields currently have sorry:

• add_assoc, zero_add, add_zero
• nsmul, nsmul_zero, nsmul_succ
• add_comm
• left_distrib, right_distrib
• zero_mul, mul_zero
• mul_assoc, one_mul, mul_one
• npow, npow_zero, npow_succ
• zsmul, zsmul_zero', zsmul_succ', zsmul_neg'
• neg_add_cancel
• mul_comm

Related Issues

• Requires resolving circular dependency with MvPolyEquiv.lean
• May need to restructure file organization

Mathlib References

• MvPolynomial.instCommRingMvPolynomial - Similar instance in Mathlib

Success Criteria

• Circular dependency is resolved
• CommRing instance is implemented and typechecks
• All ring axioms are proven (no sorrys)
• Neg and Sub operations are verified to exist

Tags

• phase-1
• api-completeness
• multivariate-polynomials
• ring-structure
• blocked (circular dependency)
• architecture (may require file restructuring)

[DimitriosMitsios]

@dhsorens This issue is blocking my work on issue #52, can I take it if no one else is working on it? I will try to split CMvPolynomial.lean in two files to avoid circular dependency.

[dhsorens]

thank you @DimitriosMitsios , yes that would be great!