feat: Implement variable renaming: rename and renameEquiv

[DimitriosMitsios]

This PR closes issue #53.

1. rename is directly implemented
2. renameEquiv is moved to Rename.lean along with the proofs of all the properties of rename

I am unsure about authorship, should I cite project authors and other contributors?

[github-actions]

🤖 Gemini PR Summary

This PR implements variable renaming capabilities for multivariate polynomials, specifically introducing the rename function and the renameEquiv ring equivalence. These changes integrate algebraic properties from Mathlib to ensure consistency with standard polynomial theory.

Features

• Variable Renaming Implementation: Introduced the rename function in CMvPolynomial to support mapping variables between different types.
• Algebraic Equivalence: Implemented renameEquiv, establishing a formal ring equivalence for variable renaming.
• Property Mapping: Leveraged Mathlib’s MvPolynomial.rename properties to establish and prove the algebraic behavior of the new renaming functions.

Refactoring

• Module Reorganization: Moved renameEquiv and its associated proofs from the core polynomial file to a dedicated module, CompPoly/Multivariate/Rename.lean, to improve maintainability.
• Code Cleanup: Removed redundant definitions of renameEquiv from the multivariate polynomial core file.
• Dependency Management: Updated the top-level CompPoly.lean to include the new Rename module in the project’s exports.

Fixes

• Issue Implement variable renaming: rename and renameEquiv #53: This PR completes the requested implementation for variable renaming functionality.

Documentation

• No explicit documentation files were updated, though the code introduces established algebraic proofs that serve as the technical specification for renaming operations.

---

Analysis of Changes

Metric	Count
📝 Files Changed	3
✅ Lines Added	308
❌ Lines Removed	9

---

sorry Tracking

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

• def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/CMvPolynomial.lean
• def renameEquiv {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Multivariate/CMvPolynomial.lean

---

🎨 **Style Guide Adherence**

The following code changes violate the CompPoly Style Guide:

CompPoly/Multivariate/CMvPolynomial.lean

• Line 226: Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum (fun i => mono.get i))
  • "Functions: Prefer fun x ↦ ... over λ x, ...." (Applies to all fun ... => syntax).
• Line 227: ExtTreeMap.foldl (fun acc mono c => acc + monomial (renameMonomial mono) c) 0 p.1
  • "Functions: Prefer fun x ↦ ... over λ x, ...."

CompPoly/Multivariate/Rename.lean

• Line 36: (g : K → V → β) (l : List (K × V)) (init : β) :
  • "Variable Conventions: ... s, t, ... : Sets or Lists" (Violation: use of l for a List).
• Line 37: List.foldl (fun acc pair => acc + g pair.1 pair.2) init l =
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
  • "Dot Notation: Use namespaces to group related definitions (e.g., List.map). This enables dot notation (e.g., l.map f) when the type is known." (Violation: use l.foldl).
• Line 38: List.foldl (fun acc pair => g pair.1 pair.2 + acc) init l := by
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
  • "Dot Notation: Use namespaces ... (e.g., l.map f)" (Violation: use l.foldl).
• Line 47: Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t =
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 48: Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 59: (Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 60: (fun i => mono.get i)) : CMvMonomial m) =
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 79, 85, 90, 125, 131, 134, 148, 151, 161, 183, 186: (Empty lines inside proofs)
  • "Empty Lines: Avoid empty lines inside definitions or proofs."
• Line 83, 138, 158, 204: rfl
  • "Dot Notation: ... Use manual dot notation for logical connectives and equality (e.g., And.intro, Eq.refl, Iff.mp)."
• Line 100: (a : CMvPolynomial n R) :
  • "Variable Conventions: a, b, c, ... : Propositions" (Violation: a used for a term/polynomial).
• Line 101, 103, 114, 117, 121, 123, 185, 197: (Multiple instances of fun ... =>)
  • "Functions: Prefer fun x ↦ ... over λ x, ...."
• Line 110, 226, 235, 244, 253: (p : CMvPolynomial n R), (p q : CMvPolynomial n R)
  • "Variable Conventions: p, q, r, ... : Predicates and relations" (Violation: p, q used for polynomials/terms; should be x, y, z).

---

📄 **Per-File Summaries**

• CompPoly.lean: Added the CompPoly.Multivariate.Rename module to the project's imports.
• CompPoly/Multivariate/CMvPolynomial.lean: Implemented the rename function for variable mapping in multivariate polynomials and removed the redundant renameEquiv definition.
• CompPoly/Multivariate/Rename.lean: Establishes algebraic properties and a ring equivalence for variable renaming in CMvPolynomial by transferring results from Mathlib's MvPolynomial.rename.

---

Last updated: 2026-02-13 13:11 UTC.

[dhsorens]

great, thanks for opening this! I will have a look at it on Monday

[dhsorens]

This is great @DimitriosMitsios , thank you. The general formula we're looking for is for a computable definition of an API function, along with a proof that it is equivalent to Mathlib's definition under the isomorphism. Plus, lots of helpful lemmas. Seeing as this is unlikely to pose any backwards compatibility issues, I'll go ahead and merge it.

[dhsorens]

@Julek I don't think this poses risks to backwards compatibility and I think the formatting on this is good. I'll go ahead and merge but will gladly do any refactoring work you need from it later.