From 84f314922c01d77856d677e066dde4a47efa0538 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Wed, 4 Feb 2026 19:23:37 +0200
Subject: [PATCH 1/6] implementation of rename

---
 CompPoly/Multivariate/CMvPolynomial.lean | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean
index d22fedb..00d853c 100644
--- a/CompPoly/Multivariate/CMvPolynomial.lean
+++ b/CompPoly/Multivariate/CMvPolynomial.lean
@@ -222,7 +222,9 @@ def bind₁ {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
 -/
 def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
     (f : Fin n → Fin m) (p : CMvPolynomial n R) : CMvPolynomial m R :=
-  sorry
+  let renameMonomial (mono : CMvMonomial n) : CMvMonomial m :=
+    Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum (fun i => mono.get i))
+  ExtTreeMap.foldl (fun acc mono c => acc + monomial (renameMonomial mono) c) 0 p.1
 
 /-- Ring equivalence for variable renaming when the function is a bijection.
 

From f653be9072d1df3dc564879e69a52f013c4c1c75 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Wed, 11 Feb 2026 11:17:45 +0200
Subject: [PATCH 2/6] All properties of rename proven, renameEquiv also
 completed

---
 CompPoly.lean                            | 1 +
 CompPoly/Multivariate/CMvPolynomial.lean | 9 +--------
 2 files changed, 2 insertions(+), 8 deletions(-)

diff --git a/CompPoly.lean b/CompPoly.lean
index 84a6ec4..e73e540 100644
--- a/CompPoly.lean
+++ b/CompPoly.lean
@@ -10,6 +10,7 @@ import CompPoly.Multivariate.CMvPolynomial
 import CompPoly.Multivariate.CMvPolynomialEvalLemmas
 import CompPoly.Multivariate.Lawful
 import CompPoly.Multivariate.MvPolyEquiv
+import CompPoly.Multivariate.Rename
 import CompPoly.Multivariate.Unlawful
 import CompPoly.Multivariate.Wheels
 import CompPoly.Univariate.Raw
diff --git a/CompPoly/Multivariate/CMvPolynomial.lean b/CompPoly/Multivariate/CMvPolynomial.lean
index 00d853c..a7b3b02 100644
--- a/CompPoly/Multivariate/CMvPolynomial.lean
+++ b/CompPoly/Multivariate/CMvPolynomial.lean
@@ -226,14 +226,7 @@ def rename {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
     Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum (fun i => mono.get i))
   ExtTreeMap.foldl (fun acc mono c => acc + monomial (renameMonomial mono) c) 0 p.1
 
-/-- Ring equivalence for variable renaming when the function is a bijection.
-
-  Given `f : Fin n ≃ Fin m`, provides a ring isomorphism between
-  `CMvPolynomial n R` and `CMvPolynomial m R`.
--/
-def renameEquiv {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
-    (f : Fin n ≃ Fin m) : CMvPolynomial n R ≃+* CMvPolynomial m R :=
-  sorry
+-- `renameEquiv` is defined in `CompPoly.Multivariate.Rename`
 
 /-- Scalar multiplication with zero handling.
 

From 5d4bfcbb905b46a8ac76e455799cb2db809980be Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Wed, 11 Feb 2026 12:34:05 +0200
Subject: [PATCH 3/6] Rename.lean file added

---
 CompPoly/Multivariate/Rename.lean | 270 ++++++++++++++++++++++++++++++
 1 file changed, 270 insertions(+)
 create mode 100644 CompPoly/Multivariate/Rename.lean

diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean
new file mode 100644
index 0000000..05f2ad6
--- /dev/null
+++ b/CompPoly/Multivariate/Rename.lean
@@ -0,0 +1,270 @@
+/-
+Copyright (c) 2025 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dimitris
+-/
+import CompPoly.Multivariate.MvPolyEquiv
+import Mathlib.Algebra.MvPolynomial.Rename
+
+/-!
+# Properties of variable renaming for `CMvPolynomial`
+
+This file proves properties of the `rename` function defined in `CMvPolynomial.lean`,
+by transferring results from Mathlib's `MvPolynomial.rename` through the
+`polyRingEquiv : CMvPolynomial n R ≃+* MvPolynomial (Fin n) R` equivalence.
+
+## Main results
+
+* `fromCMvPolynomial_rename` — correspondence between our `rename` and Mathlib's
+* `rename_C`, `rename_X`, `rename_add`, `rename_mul`, `rename_id` — algebraic properties
+* `CMvPolynomial.renameEquiv` — ring isomorphism for bijective variable renaming
+
+-/
+
+namespace CPoly
+
+open Std CMvPolynomial
+
+variable {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
+
+/-! ### Helper lemmas for `fromCMvPolynomial_rename` -/
+
+/-- In a commutative additive monoid, the order of addition in a list fold doesn't matter. -/
+private lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β]
+    (g : K → V → β) (l : List (K × V)) (init : β) :
+    List.foldl (fun acc pair => acc + g pair.1 pair.2) init l =
+    List.foldl (fun acc pair => g pair.1 pair.2 + acc) init l := by
+  induction l generalizing init with
+  | nil => rfl
+  | cons h t ih =>
+    simp only [List.foldl_cons]
+    rw [show init + g h.1 h.2 = g h.1 h.2 + init from add_comm _ _]
+    exact ih _
+
+/-- Swapping addition order in `ExtTreeMap.foldl` doesn't change the result. -/
+private lemma foldl_add_comm' {β : Type} [AddCommMonoid β] {k : ℕ}
+    {R' : Type} (g : CMvMonomial k → R' → β) (t : Std.ExtTreeMap (CMvMonomial k) R') :
+    Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t =
+    Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by
+  simp only [Std.ExtTreeMap.foldl_eq_foldl_toList]
+  exact list_foldl_add_comm g t.toList 0
+
+/-- The renaming of a monomial corresponds to `Finsupp.mapDomain` on the Finsupp side. -/
+private lemma toFinsupp_apply (mono : CMvMonomial n) (i : Fin n) :
+    (CMvMonomial.toFinsupp mono) i = mono.get i := rfl
+
+private lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) :
+    (Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum
+      (fun i => mono.get i)) : CMvMonomial m) =
+    CMvMonomial.ofFinsupp (Finsupp.mapDomain f (CMvMonomial.toFinsupp mono)) := by
+  unfold CMvMonomial.ofFinsupp
+  congr 1; funext j
+  -- Goal: ∑ i with f i = j, mono.get i = (mapDomain f (toFinsupp mono)) j
+  simp only [Finsupp.mapDomain, Finsupp.sum_apply, Finsupp.single_apply]
+  -- Now: ∑ i with f i = j, mono.get i = mono.toFinsupp.sum fun a₁ b => if f a₁ = j then b else 0
+  -- Convert LHS filter to if-then-else
+  rw [Finset.sum_filter]
+  -- Now: ∑ i in univ, if f i = j then mono.get i else 0 = Finsupp.sum ...
+  -- Unfold Finsupp.sum on RHS
+  rw [Finsupp.sum]
+  -- Now: ∑ i in univ, if ... = ∑ a in support, if f a = j then (toFinsupp mono) a else 0
+  -- (toFinsupp mono) a = mono.get a by definition
+  symm
+  apply Finset.sum_subset (Finset.subset_univ _)
+  intro x _ hxs
+  rw [Finsupp.notMem_support_iff] at hxs
+  -- hxs : (toFinsupp mono) x = 0, which is definitionally mono.get x = 0
+  simp [hxs]
+
+/-- `fromCMvPolynomial` applied to our `monomial` gives Mathlib's `MvPolynomial.monomial`. -/
+private lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) :
+    fromCMvPolynomial (CMvPolynomial.monomial mono c) =
+    MvPolynomial.monomial (CMvMonomial.toFinsupp mono) c := by
+  by_cases hc : c = 0
+  · subst hc; simp [CMvPolynomial.monomial, map_zero]
+  · ext μ
+    rw [coeff_eq, MvPolynomial.coeff_monomial]
+    -- Goal: coeff (ofFinsupp μ) (monomial mono c) = if toFinsupp mono = μ then c else 0
+    unfold CMvPolynomial.coeff CMvPolynomial.monomial
+    simp only [show (c == (0 : R)) = false from by simp [hc]]
+    -- Now dealing with: (fromUnlawful (ofList [(mono, c)])).1[ofFinsupp μ]?.getD 0
+    unfold Lawful.fromUnlawful
+    erw [Unlawful.filter_get]
+    simp only [Unlawful.ofList]
+    by_cases hm : CMvMonomial.toFinsupp mono = μ
+    · -- ofFinsupp μ = mono, lookup should give c
+      subst hm; rw [if_pos rfl, CMvMonomial.ofFinsupp_toFinsupp]
+      erw [ExtTreeMap.getElem?_ofList_of_mem
+        (k := mono) (k_eq := compare_self) (v := c)
+        (mem := by simp) (distinct := ?distinct)]
+      · simp
+      case distinct => simp
+    · -- ofFinsupp μ ≠ mono, lookup should give none
+      rw [if_neg hm]
+      have hne : CMvMonomial.ofFinsupp μ ≠ mono :=
+        fun h => hm (h ▸ CMvMonomial.toFinsupp_ofFinsupp)
+      erw [ExtTreeMap.getElem?_ofList_of_contains_eq_false (by simp [hne])]
+      rfl
+
+/-- `fromCMvPolynomial` distributes over `Finsupp.sum` (generalized to different dimensions). -/
+private lemma fromCMvPolynomial_finsupp_sum {k : ℕ}
+    (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) (a : CMvPolynomial n R) :
+    fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) =
+    Finsupp.sum (fromCMvPolynomial a) (fun μ c => fromCMvPolynomial (g μ c)) := by
+  unfold Finsupp.sum; ext
+  simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]
+
+/-! ### Main correspondence lemma -/
+
+/-- Correspondence: our `rename` agrees with Mathlib's `MvPolynomial.rename`
+    under the `fromCMvPolynomial` equivalence. -/
+lemma fromCMvPolynomial_rename (f : Fin n → Fin m) (p : CMvPolynomial n R) :
+    fromCMvPolynomial (CMvPolynomial.rename f p) =
+    MvPolynomial.rename f (fromCMvPolynomial p) := by
+  -- Step 1: Express rename as Finsupp.sum via foldl_add_comm + foldl_eq_sum
+  have step1 : CMvPolynomial.rename f p =
+      Finsupp.sum (fromCMvPolynomial p) (fun μ c =>
+        CMvPolynomial.monomial (CMvMonomial.ofFinsupp (Finsupp.mapDomain f μ)) c) := by
+    -- Inline the let binding and rewrite renameMonomial
+    show Std.ExtTreeMap.foldl (fun acc mono c => acc + CMvPolynomial.monomial
+        (Vector.ofFn fun j => (Finset.univ.filter fun i => f i = j).sum fun i => mono.get i) c)
+        0 p.1 = _
+    simp_rw [renameMonomial_eq f]
+    rw [foldl_add_comm' (fun mono c =>
+      CMvPolynomial.monomial (CMvMonomial.ofFinsupp
+        (Finsupp.mapDomain f (CMvMonomial.toFinsupp mono))) c)]
+    rw [foldl_eq_sum]
+    congr 1; ext μ c
+    simp only [Function.comp_def, CMvMonomial.toFinsupp_ofFinsupp]
+  rw [step1]
+  -- Step 2: Distribute fromCMvPolynomial over the Finsupp.sum
+  rw [fromCMvPolynomial_finsupp_sum]
+  -- Step 3: Simplify each term using fromCMvPolynomial_monomial + toFinsupp_ofFinsupp
+  simp only [fromCMvPolynomial_monomial, CMvMonomial.toFinsupp_ofFinsupp]
+  -- Step 4: Use Mathlib's rename_monomial to connect to rename
+  conv_rhs =>
+    rw [← MvPolynomial.support_sum_monomial_coeff (fromCMvPolynomial p)]
+    rw [map_sum (MvPolynomial.rename f)]
+  simp only [MvPolynomial.rename_monomial]
+  rfl
+
+/-! ### Bridging lemmas for C and X -/
+
+/-- Our constant `C c` equals `monomial 0 c`. -/
+private lemma C_eq_monomial {k : ℕ} (c : R) :
+    CMvPolynomial.C (n := k) c = CMvPolynomial.monomial 0 c := by
+  by_cases hc : c = 0
+  · subst hc; ext m
+    unfold CMvPolynomial.coeff CMvPolynomial.C CMvPolynomial.monomial Lawful.C Unlawful.C
+    grind
+  · ext m
+    show (CMvPolynomial.C c).coeff m = (CMvPolynomial.monomial (0 : CMvMonomial k) c).coeff m
+    unfold CMvPolynomial.coeff CMvPolynomial.C Lawful.C CMvPolynomial.monomial Unlawful.C
+    simp only [show (c == (0 : R)) = false from by simp [hc], hc, ite_false, MonoR.C]
+    show (Unlawful.ofList [(CMvMonomial.zero, c)])[m]?.getD 0 =
+      (Lawful.fromUnlawful (Unlawful.ofList [(CMvMonomial.zero, c)])).1[m]?.getD 0
+    unfold Lawful.fromUnlawful
+    erw [Unlawful.filter_get]
+
+private lemma toFinsupp_zero {k : ℕ} :
+    CMvMonomial.toFinsupp (0 : CMvMonomial k) = 0 := by
+  ext i
+  simp [CMvMonomial.toFinsupp, Vector.get]
+
+/-- `fromCMvPolynomial` maps our `C` to Mathlib's `C`. -/
+private lemma fromCMvPolynomial_C {k : ℕ} (c : R) :
+    fromCMvPolynomial (CMvPolynomial.C (n := k) c) = MvPolynomial.C c := by
+  rw [C_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_zero,
+      ← MvPolynomial.C_apply]
+
+/-! ### Algebraic properties of rename -/
+
+/-- Constants are unchanged under renaming. -/
+@[simp]
+lemma rename_C (f : Fin n → Fin m) (c : R) :
+    CMvPolynomial.rename f (CMvPolynomial.C c) = CMvPolynomial.C (n := m) c := by
+  apply fromCMvPolynomial_injective
+  rw [fromCMvPolynomial_rename, fromCMvPolynomial_C, fromCMvPolynomial_C]
+  exact MvPolynomial.rename_C f c
+
+/-- `X i` is a special case of `monomial`. -/
+private lemma X_eq_monomial {k : ℕ} (i : Fin k) :
+    CMvPolynomial.X (R := R) i = CMvPolynomial.monomial
+      (Vector.ofFn (fun j => if j = i then 1 else 0)) (1 : R) := by
+  unfold CMvPolynomial.X CMvPolynomial.monomial
+  by_cases h : (1 : R) = 0
+  · -- Zero ring
+    ext m; unfold CMvPolynomial.coeff Lawful.fromUnlawful
+    erw [Unlawful.filter_get]; simp [h]; grind
+  · -- 1 ≠ 0, so (1 == 0) = false, and both sides are fromUnlawful(ofList[...])
+    simp only [show ((1 : R) == 0) = false from by simp [h]]
+    exact (if_neg (by decide)).symm
+
+/-- The Finsupp of the unit monomial at `i` is `Finsupp.single i 1`. -/
+private lemma toFinsupp_unitMono {k : ℕ} (i : Fin k) :
+    CMvMonomial.toFinsupp (Vector.ofFn (fun j : Fin k => if j = i then 1 else 0)) =
+    Finsupp.single i 1 := by
+  ext j
+  simp [CMvMonomial.toFinsupp, Vector.get, Finsupp.single_apply, eq_comm]
+
+/-- `fromCMvPolynomial` maps our `X i` to Mathlib's `X i`. -/
+private lemma fromCMvPolynomial_X {k : ℕ} (i : Fin k) :
+    fromCMvPolynomial (CMvPolynomial.X (R := R) i) = MvPolynomial.X i := by
+  rw [X_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_unitMono]
+  rfl
+
+/-- Renaming maps variable `X i` to `X (f i)`. -/
+@[simp]
+lemma rename_X (f : Fin n → Fin m) (i : Fin n) :
+    CMvPolynomial.rename f (CMvPolynomial.X (R := R) i) = CMvPolynomial.X (f i) := by
+  apply fromCMvPolynomial_injective
+  rw [fromCMvPolynomial_rename, fromCMvPolynomial_X, fromCMvPolynomial_X]
+  exact MvPolynomial.rename_X f i
+
+/-- Renaming preserves addition. -/
+@[simp]
+lemma rename_add (f : Fin n → Fin m) (p q : CMvPolynomial n R) :
+    CMvPolynomial.rename f (p + q) =
+    CMvPolynomial.rename f p + CMvPolynomial.rename f q := by
+  apply fromCMvPolynomial_injective
+  simp only [fromCMvPolynomial_rename, CPoly.map_add]
+  exact _root_.map_add (MvPolynomial.rename f) (fromCMvPolynomial p) (fromCMvPolynomial q)
+
+/-- Renaming preserves multiplication. -/
+@[simp]
+lemma rename_mul (f : Fin n → Fin m) (p q : CMvPolynomial n R) :
+    CMvPolynomial.rename f (p * q) =
+    CMvPolynomial.rename f p * CMvPolynomial.rename f q := by
+  apply fromCMvPolynomial_injective
+  simp only [fromCMvPolynomial_rename, CPoly.map_mul]
+  exact _root_.map_mul (MvPolynomial.rename f) (fromCMvPolynomial p) (fromCMvPolynomial q)
+
+/-- Renaming by the identity function is the identity. -/
+@[simp]
+lemma rename_id (p : CMvPolynomial n R) :
+    CMvPolynomial.rename id p = p := by
+  apply fromCMvPolynomial_injective
+  rw [fromCMvPolynomial_rename]
+  exact MvPolynomial.rename_id_apply (fromCMvPolynomial p)
+
+/-- Composing two renamings is the same as renaming by the composition. -/
+@[simp]
+lemma rename_rename {k : ℕ} (f : Fin n → Fin m) (g : Fin m → Fin k)
+    (p : CMvPolynomial n R) :
+    CMvPolynomial.rename g (CMvPolynomial.rename f p) =
+    CMvPolynomial.rename (g ∘ f) p := by
+  apply fromCMvPolynomial_injective
+  rw [fromCMvPolynomial_rename, fromCMvPolynomial_rename, fromCMvPolynomial_rename]
+  exact MvPolynomial.rename_rename f g (fromCMvPolynomial p)
+
+/-- Ring equivalence for variable renaming when the function is a bijection. -/
+noncomputable def CMvPolynomial.renameEquiv (f : Fin n ≃ Fin m) :
+    CMvPolynomial n R ≃+* CMvPolynomial m R where
+  toFun := CMvPolynomial.rename f
+  invFun := CMvPolynomial.rename f.symm
+  left_inv p := by rw [rename_rename, f.symm_comp_self, rename_id]
+  right_inv q := by rw [rename_rename, f.self_comp_symm, rename_id]
+  map_add' p q := rename_add f p q
+  map_mul' p q := rename_mul f p q
+
+end CPoly

From 45dd6511235db28522e259ea15f88e680233171e Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Wed, 11 Feb 2026 19:47:44 +0200
Subject: [PATCH 4/6] Removed private lemma and added some cleaning.

---
 CompPoly/Multivariate/Rename.lean | 32 ++++++++++++++++---------------
 1 file changed, 17 insertions(+), 15 deletions(-)

diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean
index 05f2ad6..5c4e6e7 100644
--- a/CompPoly/Multivariate/Rename.lean
+++ b/CompPoly/Multivariate/Rename.lean
@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2025 CompPoly. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dimitris
+Authors: Dimitris Mitsios
 -/
 import CompPoly.Multivariate.MvPolyEquiv
 import Mathlib.Algebra.MvPolynomial.Rename
@@ -16,7 +16,7 @@ by transferring results from Mathlib's `MvPolynomial.rename` through the
 ## Main results
 
 * `fromCMvPolynomial_rename` — correspondence between our `rename` and Mathlib's
-* `rename_C`, `rename_X`, `rename_add`, `rename_mul`, `rename_id` — algebraic properties
+* `rename_C`, `rename_X`, `rename_add`, `rename_mul`, `rename_id`, `rename_rename` — algebraic properties
 * `CMvPolynomial.renameEquiv` — ring isomorphism for bijective variable renaming
 
 -/
@@ -30,7 +30,7 @@ variable {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
 /-! ### Helper lemmas for `fromCMvPolynomial_rename` -/
 
 /-- In a commutative additive monoid, the order of addition in a list fold doesn't matter. -/
-private lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β]
+lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β]
     (g : K → V → β) (l : List (K × V)) (init : β) :
     List.foldl (fun acc pair => acc + g pair.1 pair.2) init l =
     List.foldl (fun acc pair => g pair.1 pair.2 + acc) init l := by
@@ -42,18 +42,19 @@ private lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β]
     exact ih _
 
 /-- Swapping addition order in `ExtTreeMap.foldl` doesn't change the result. -/
-private lemma foldl_add_comm' {β : Type} [AddCommMonoid β] {k : ℕ}
+lemma foldl_add_comm' {β : Type} [AddCommMonoid β] {k : ℕ}
     {R' : Type} (g : CMvMonomial k → R' → β) (t : Std.ExtTreeMap (CMvMonomial k) R') :
     Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t =
     Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by
   simp only [Std.ExtTreeMap.foldl_eq_foldl_toList]
   exact list_foldl_add_comm g t.toList 0
 
-/-- The renaming of a monomial corresponds to `Finsupp.mapDomain` on the Finsupp side. -/
-private lemma toFinsupp_apply (mono : CMvMonomial n) (i : Fin n) :
+/-- Applying `CMvMonomial.toFinsupp` at index `i` equals `Vector.get`. -/
+lemma toFinsupp_apply (mono : CMvMonomial n) (i : Fin n) :
     (CMvMonomial.toFinsupp mono) i = mono.get i := rfl
 
-private lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) :
+/-- The renaming of a monomial corresponds to `Finsupp.mapDomain` on the Finsupp side. -/
+lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) :
     (Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum
       (fun i => mono.get i)) : CMvMonomial m) =
     CMvMonomial.ofFinsupp (Finsupp.mapDomain f (CMvMonomial.toFinsupp mono)) := by
@@ -77,7 +78,7 @@ private lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) :
   simp [hxs]
 
 /-- `fromCMvPolynomial` applied to our `monomial` gives Mathlib's `MvPolynomial.monomial`. -/
-private lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) :
+lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) :
     fromCMvPolynomial (CMvPolynomial.monomial mono c) =
     MvPolynomial.monomial (CMvMonomial.toFinsupp mono) c := by
   by_cases hc : c = 0
@@ -107,7 +108,7 @@ private lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R
       rfl
 
 /-- `fromCMvPolynomial` distributes over `Finsupp.sum` (generalized to different dimensions). -/
-private lemma fromCMvPolynomial_finsupp_sum {k : ℕ}
+lemma fromCMvPolynomial_finsupp_sum {k : ℕ}
     (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) (a : CMvPolynomial n R) :
     fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) =
     Finsupp.sum (fromCMvPolynomial a) (fun μ c => fromCMvPolynomial (g μ c)) := by
@@ -151,7 +152,7 @@ lemma fromCMvPolynomial_rename (f : Fin n → Fin m) (p : CMvPolynomial n R) :
 /-! ### Bridging lemmas for C and X -/
 
 /-- Our constant `C c` equals `monomial 0 c`. -/
-private lemma C_eq_monomial {k : ℕ} (c : R) :
+lemma C_eq_monomial {k : ℕ} (c : R) :
     CMvPolynomial.C (n := k) c = CMvPolynomial.monomial 0 c := by
   by_cases hc : c = 0
   · subst hc; ext m
@@ -166,13 +167,14 @@ private lemma C_eq_monomial {k : ℕ} (c : R) :
     unfold Lawful.fromUnlawful
     erw [Unlawful.filter_get]
 
-private lemma toFinsupp_zero {k : ℕ} :
+/-- The `Finsupp` of the zero monomial is zero. -/
+lemma toFinsupp_zero {k : ℕ} :
     CMvMonomial.toFinsupp (0 : CMvMonomial k) = 0 := by
   ext i
   simp [CMvMonomial.toFinsupp, Vector.get]
 
 /-- `fromCMvPolynomial` maps our `C` to Mathlib's `C`. -/
-private lemma fromCMvPolynomial_C {k : ℕ} (c : R) :
+lemma fromCMvPolynomial_C {k : ℕ} (c : R) :
     fromCMvPolynomial (CMvPolynomial.C (n := k) c) = MvPolynomial.C c := by
   rw [C_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_zero,
       ← MvPolynomial.C_apply]
@@ -188,7 +190,7 @@ lemma rename_C (f : Fin n → Fin m) (c : R) :
   exact MvPolynomial.rename_C f c
 
 /-- `X i` is a special case of `monomial`. -/
-private lemma X_eq_monomial {k : ℕ} (i : Fin k) :
+lemma X_eq_monomial {k : ℕ} (i : Fin k) :
     CMvPolynomial.X (R := R) i = CMvPolynomial.monomial
       (Vector.ofFn (fun j => if j = i then 1 else 0)) (1 : R) := by
   unfold CMvPolynomial.X CMvPolynomial.monomial
@@ -201,14 +203,14 @@ private lemma X_eq_monomial {k : ℕ} (i : Fin k) :
     exact (if_neg (by decide)).symm
 
 /-- The Finsupp of the unit monomial at `i` is `Finsupp.single i 1`. -/
-private lemma toFinsupp_unitMono {k : ℕ} (i : Fin k) :
+lemma toFinsupp_unitMono {k : ℕ} (i : Fin k) :
     CMvMonomial.toFinsupp (Vector.ofFn (fun j : Fin k => if j = i then 1 else 0)) =
     Finsupp.single i 1 := by
   ext j
   simp [CMvMonomial.toFinsupp, Vector.get, Finsupp.single_apply, eq_comm]
 
 /-- `fromCMvPolynomial` maps our `X i` to Mathlib's `X i`. -/
-private lemma fromCMvPolynomial_X {k : ℕ} (i : Fin k) :
+lemma fromCMvPolynomial_X {k : ℕ} (i : Fin k) :
     fromCMvPolynomial (CMvPolynomial.X (R := R) i) = MvPolynomial.X i := by
   rw [X_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_unitMono]
   rfl

From 3af359d50e38a3a513983b8edb371572909863d9 Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Fri, 13 Feb 2026 13:21:57 +0200
Subject: [PATCH 5/6]  comments cleaned up

---
 CompPoly/Multivariate/Rename.lean | 188 +++++++++++++++++-------------
 1 file changed, 109 insertions(+), 79 deletions(-)

diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean
index 5c4e6e7..2d714c0 100644
--- a/CompPoly/Multivariate/Rename.lean
+++ b/CompPoly/Multivariate/Rename.lean
@@ -1,7 +1,6 @@
 /-
 Copyright (c) 2025 CompPoly. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Dimitris Mitsios
 -/
 import CompPoly.Multivariate.MvPolyEquiv
 import Mathlib.Algebra.MvPolynomial.Rename
@@ -15,8 +14,10 @@ by transferring results from Mathlib's `MvPolynomial.rename` through the
 
 ## Main results
 
-* `fromCMvPolynomial_rename` — correspondence between our `rename` and Mathlib's
-* `rename_C`, `rename_X`, `rename_add`, `rename_mul`, `rename_id`, `rename_rename` — algebraic properties
+* `fromCMvPolynomial_rename` — correspondence between `CMvPolynomial.rename` and
+  `MvPolynomial.rename`
+* `rename_C`, `rename_X`, `rename_add`, `rename_mul`, `rename_id`, `rename_rename`
+  — algebraic properties
 * `CMvPolynomial.renameEquiv` — ring isomorphism for bijective variable renaming
 
 -/
@@ -29,7 +30,8 @@ variable {n m : ℕ} {R : Type} [CommSemiring R] [BEq R] [LawfulBEq R]
 
 /-! ### Helper lemmas for `fromCMvPolynomial_rename` -/
 
-/-- In a commutative additive monoid, the order of addition in a list fold doesn't matter. -/
+/-- In a commutative additive monoid, the order of addition in a list fold
+does not matter. -/
 lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β]
     (g : K → V → β) (l : List (K × V)) (init : β) :
     List.foldl (fun acc pair => acc + g pair.1 pair.2) init l =
@@ -41,9 +43,10 @@ lemma list_foldl_add_comm {β K V : Type} [AddCommMonoid β]
     rw [show init + g h.1 h.2 = g h.1 h.2 + init from add_comm _ _]
     exact ih _
 
-/-- Swapping addition order in `ExtTreeMap.foldl` doesn't change the result. -/
+/-- Swapping addition order in `ExtTreeMap.foldl` does not change the result. -/
 lemma foldl_add_comm' {β : Type} [AddCommMonoid β] {k : ℕ}
-    {R' : Type} (g : CMvMonomial k → R' → β) (t : Std.ExtTreeMap (CMvMonomial k) R') :
+    {R' : Type} (g : CMvMonomial k → R' → β)
+    (t : Std.ExtTreeMap (CMvMonomial k) R') :
     Std.ExtTreeMap.foldl (fun acc m c => acc + g m c) (0 : β) t =
     Std.ExtTreeMap.foldl (fun acc m c => g m c + acc) (0 : β) t := by
   simp only [Std.ExtTreeMap.foldl_eq_foldl_toList]
@@ -53,31 +56,27 @@ lemma foldl_add_comm' {β : Type} [AddCommMonoid β] {k : ℕ}
 lemma toFinsupp_apply (mono : CMvMonomial n) (i : Fin n) :
     (CMvMonomial.toFinsupp mono) i = mono.get i := rfl
 
-/-- The renaming of a monomial corresponds to `Finsupp.mapDomain` on the Finsupp side. -/
+/-- Monomial renaming via `Vector.ofFn` corresponds to `Finsupp.mapDomain`
+on the `Finsupp` side. -/
 lemma renameMonomial_eq (f : Fin n → Fin m) (mono : CMvMonomial n) :
     (Vector.ofFn (fun j => (Finset.univ.filter (fun i => f i = j)).sum
       (fun i => mono.get i)) : CMvMonomial m) =
-    CMvMonomial.ofFinsupp (Finsupp.mapDomain f (CMvMonomial.toFinsupp mono)) := by
+    CMvMonomial.ofFinsupp
+      (Finsupp.mapDomain f (CMvMonomial.toFinsupp mono)) := by
   unfold CMvMonomial.ofFinsupp
   congr 1; funext j
-  -- Goal: ∑ i with f i = j, mono.get i = (mapDomain f (toFinsupp mono)) j
   simp only [Finsupp.mapDomain, Finsupp.sum_apply, Finsupp.single_apply]
-  -- Now: ∑ i with f i = j, mono.get i = mono.toFinsupp.sum fun a₁ b => if f a₁ = j then b else 0
-  -- Convert LHS filter to if-then-else
   rw [Finset.sum_filter]
-  -- Now: ∑ i in univ, if f i = j then mono.get i else 0 = Finsupp.sum ...
-  -- Unfold Finsupp.sum on RHS
   rw [Finsupp.sum]
-  -- Now: ∑ i in univ, if ... = ∑ a in support, if f a = j then (toFinsupp mono) a else 0
-  -- (toFinsupp mono) a = mono.get a by definition
+  -- Extend the sum from `support` to `Finset.univ`
   symm
   apply Finset.sum_subset (Finset.subset_univ _)
   intro x _ hxs
   rw [Finsupp.notMem_support_iff] at hxs
-  -- hxs : (toFinsupp mono) x = 0, which is definitionally mono.get x = 0
   simp [hxs]
 
-/-- `fromCMvPolynomial` applied to our `monomial` gives Mathlib's `MvPolynomial.monomial`. -/
+/-- `fromCMvPolynomial` maps `CMvPolynomial.monomial` to
+`MvPolynomial.monomial`. -/
 lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) :
     fromCMvPolynomial (CMvPolynomial.monomial mono c) =
     MvPolynomial.monomial (CMvMonomial.toFinsupp mono) c := by
@@ -85,50 +84,53 @@ lemma fromCMvPolynomial_monomial {k : ℕ} (mono : CMvMonomial k) (c : R) :
   · subst hc; simp [CMvPolynomial.monomial, map_zero]
   · ext μ
     rw [coeff_eq, MvPolynomial.coeff_monomial]
-    -- Goal: coeff (ofFinsupp μ) (monomial mono c) = if toFinsupp mono = μ then c else 0
     unfold CMvPolynomial.coeff CMvPolynomial.monomial
     simp only [show (c == (0 : R)) = false from by simp [hc]]
-    -- Now dealing with: (fromUnlawful (ofList [(mono, c)])).1[ofFinsupp μ]?.getD 0
     unfold Lawful.fromUnlawful
     erw [Unlawful.filter_get]
     simp only [Unlawful.ofList]
     by_cases hm : CMvMonomial.toFinsupp mono = μ
-    · -- ofFinsupp μ = mono, lookup should give c
-      subst hm; rw [if_pos rfl, CMvMonomial.ofFinsupp_toFinsupp]
+    · subst hm; rw [if_pos rfl, CMvMonomial.ofFinsupp_toFinsupp]
       erw [ExtTreeMap.getElem?_ofList_of_mem
         (k := mono) (k_eq := compare_self) (v := c)
         (mem := by simp) (distinct := ?distinct)]
       · simp
       case distinct => simp
-    · -- ofFinsupp μ ≠ mono, lookup should give none
-      rw [if_neg hm]
+    · rw [if_neg hm]
       have hne : CMvMonomial.ofFinsupp μ ≠ mono :=
         fun h => hm (h ▸ CMvMonomial.toFinsupp_ofFinsupp)
-      erw [ExtTreeMap.getElem?_ofList_of_contains_eq_false (by simp [hne])]
+      erw [ExtTreeMap.getElem?_ofList_of_contains_eq_false
+        (by simp [hne])]
       rfl
 
-/-- `fromCMvPolynomial` distributes over `Finsupp.sum` (generalized to different dimensions). -/
+/-- `fromCMvPolynomial` distributes over `Finsupp.sum`. -/
 lemma fromCMvPolynomial_finsupp_sum {k : ℕ}
-    (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R) (a : CMvPolynomial n R) :
+    (g : (Fin n →₀ ℕ) → R → CMvPolynomial k R)
+    (a : CMvPolynomial n R) :
     fromCMvPolynomial (Finsupp.sum (fromCMvPolynomial a) g) =
-    Finsupp.sum (fromCMvPolynomial a) (fun μ c => fromCMvPolynomial (g μ c)) := by
+    Finsupp.sum (fromCMvPolynomial a)
+      (fun μ c => fromCMvPolynomial (g μ c)) := by
   unfold Finsupp.sum; ext
   simp [MvPolynomial.coeff_sum, coeff_eq, coeff_sum]
 
 /-! ### Main correspondence lemma -/
 
-/-- Correspondence: our `rename` agrees with Mathlib's `MvPolynomial.rename`
-    under the `fromCMvPolynomial` equivalence. -/
-lemma fromCMvPolynomial_rename (f : Fin n → Fin m) (p : CMvPolynomial n R) :
+/-- `CMvPolynomial.rename` agrees with `MvPolynomial.rename` under the
+`fromCMvPolynomial` equivalence. -/
+lemma fromCMvPolynomial_rename (f : Fin n → Fin m)
+    (p : CMvPolynomial n R) :
     fromCMvPolynomial (CMvPolynomial.rename f p) =
     MvPolynomial.rename f (fromCMvPolynomial p) := by
-  -- Step 1: Express rename as Finsupp.sum via foldl_add_comm + foldl_eq_sum
+  -- Express rename as a `Finsupp.sum` via `foldl_eq_sum`
   have step1 : CMvPolynomial.rename f p =
       Finsupp.sum (fromCMvPolynomial p) (fun μ c =>
-        CMvPolynomial.monomial (CMvMonomial.ofFinsupp (Finsupp.mapDomain f μ)) c) := by
-    -- Inline the let binding and rewrite renameMonomial
-    show Std.ExtTreeMap.foldl (fun acc mono c => acc + CMvPolynomial.monomial
-        (Vector.ofFn fun j => (Finset.univ.filter fun i => f i = j).sum fun i => mono.get i) c)
+        CMvPolynomial.monomial
+          (CMvMonomial.ofFinsupp (Finsupp.mapDomain f μ)) c) := by
+    show Std.ExtTreeMap.foldl
+        (fun acc mono c => acc + CMvPolynomial.monomial
+          (Vector.ofFn fun j =>
+            (Finset.univ.filter fun i => f i = j).sum
+              fun i => mono.get i) c)
         0 p.1 = _
     simp_rw [renameMonomial_eq f]
     rw [foldl_add_comm' (fun mono c =>
@@ -138,32 +140,37 @@ lemma fromCMvPolynomial_rename (f : Fin n → Fin m) (p : CMvPolynomial n R) :
     congr 1; ext μ c
     simp only [Function.comp_def, CMvMonomial.toFinsupp_ofFinsupp]
   rw [step1]
-  -- Step 2: Distribute fromCMvPolynomial over the Finsupp.sum
   rw [fromCMvPolynomial_finsupp_sum]
-  -- Step 3: Simplify each term using fromCMvPolynomial_monomial + toFinsupp_ofFinsupp
-  simp only [fromCMvPolynomial_monomial, CMvMonomial.toFinsupp_ofFinsupp]
-  -- Step 4: Use Mathlib's rename_monomial to connect to rename
+  simp only [fromCMvPolynomial_monomial,
+    CMvMonomial.toFinsupp_ofFinsupp]
+  -- Conclude using Mathlib's `MvPolynomial.rename_monomial`
   conv_rhs =>
-    rw [← MvPolynomial.support_sum_monomial_coeff (fromCMvPolynomial p)]
+    rw [← MvPolynomial.support_sum_monomial_coeff
+      (fromCMvPolynomial p)]
     rw [map_sum (MvPolynomial.rename f)]
   simp only [MvPolynomial.rename_monomial]
   rfl
 
-/-! ### Bridging lemmas for C and X -/
+/-! ### Bridging lemmas for `C` and `X` -/
 
-/-- Our constant `C c` equals `monomial 0 c`. -/
+/-- `CMvPolynomial.C c` equals `CMvPolynomial.monomial 0 c`. -/
 lemma C_eq_monomial {k : ℕ} (c : R) :
     CMvPolynomial.C (n := k) c = CMvPolynomial.monomial 0 c := by
   by_cases hc : c = 0
   · subst hc; ext m
-    unfold CMvPolynomial.coeff CMvPolynomial.C CMvPolynomial.monomial Lawful.C Unlawful.C
+    unfold CMvPolynomial.coeff CMvPolynomial.C CMvPolynomial.monomial
+      Lawful.C Unlawful.C
     grind
   · ext m
-    show (CMvPolynomial.C c).coeff m = (CMvPolynomial.monomial (0 : CMvMonomial k) c).coeff m
-    unfold CMvPolynomial.coeff CMvPolynomial.C Lawful.C CMvPolynomial.monomial Unlawful.C
-    simp only [show (c == (0 : R)) = false from by simp [hc], hc, ite_false, MonoR.C]
+    show (CMvPolynomial.C c).coeff m =
+      (CMvPolynomial.monomial (0 : CMvMonomial k) c).coeff m
+    unfold CMvPolynomial.coeff CMvPolynomial.C Lawful.C
+      CMvPolynomial.monomial Unlawful.C
+    simp only [show (c == (0 : R)) = false from by simp [hc],
+      hc, ite_false, MonoR.C]
     show (Unlawful.ofList [(CMvMonomial.zero, c)])[m]?.getD 0 =
-      (Lawful.fromUnlawful (Unlawful.ofList [(CMvMonomial.zero, c)])).1[m]?.getD 0
+      (Lawful.fromUnlawful
+        (Unlawful.ofList [(CMvMonomial.zero, c)])).1[m]?.getD 0
     unfold Lawful.fromUnlawful
     erw [Unlawful.filter_get]
 
@@ -173,9 +180,10 @@ lemma toFinsupp_zero {k : ℕ} :
   ext i
   simp [CMvMonomial.toFinsupp, Vector.get]
 
-/-- `fromCMvPolynomial` maps our `C` to Mathlib's `C`. -/
+/-- `fromCMvPolynomial` maps `CMvPolynomial.C` to `MvPolynomial.C`. -/
 lemma fromCMvPolynomial_C {k : ℕ} (c : R) :
-    fromCMvPolynomial (CMvPolynomial.C (n := k) c) = MvPolynomial.C c := by
+    fromCMvPolynomial (CMvPolynomial.C (n := k) c) =
+    MvPolynomial.C c := by
   rw [C_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_zero,
       ← MvPolynomial.C_apply]
 
@@ -184,62 +192,79 @@ lemma fromCMvPolynomial_C {k : ℕ} (c : R) :
 /-- Constants are unchanged under renaming. -/
 @[simp]
 lemma rename_C (f : Fin n → Fin m) (c : R) :
-    CMvPolynomial.rename f (CMvPolynomial.C c) = CMvPolynomial.C (n := m) c := by
+    CMvPolynomial.rename f (CMvPolynomial.C c) =
+    CMvPolynomial.C (n := m) c := by
   apply fromCMvPolynomial_injective
-  rw [fromCMvPolynomial_rename, fromCMvPolynomial_C, fromCMvPolynomial_C]
+  rw [fromCMvPolynomial_rename, fromCMvPolynomial_C,
+    fromCMvPolynomial_C]
   exact MvPolynomial.rename_C f c
 
-/-- `X i` is a special case of `monomial`. -/
+/-- `CMvPolynomial.X i` equals `CMvPolynomial.monomial eᵢ 1`
+where `eᵢ` is the `i`-th standard basis vector. -/
 lemma X_eq_monomial {k : ℕ} (i : Fin k) :
     CMvPolynomial.X (R := R) i = CMvPolynomial.monomial
-      (Vector.ofFn (fun j => if j = i then 1 else 0)) (1 : R) := by
+      (Vector.ofFn (fun j => if j = i then 1 else 0))
+      (1 : R) := by
   unfold CMvPolynomial.X CMvPolynomial.monomial
   by_cases h : (1 : R) = 0
-  · -- Zero ring
-    ext m; unfold CMvPolynomial.coeff Lawful.fromUnlawful
+  · ext m; unfold CMvPolynomial.coeff Lawful.fromUnlawful
     erw [Unlawful.filter_get]; simp [h]; grind
-  · -- 1 ≠ 0, so (1 == 0) = false, and both sides are fromUnlawful(ofList[...])
-    simp only [show ((1 : R) == 0) = false from by simp [h]]
+  · simp only [show ((1 : R) == 0) = false from by simp [h]]
     exact (if_neg (by decide)).symm
 
-/-- The Finsupp of the unit monomial at `i` is `Finsupp.single i 1`. -/
+/-- The `Finsupp` of the `i`-th standard basis monomial is
+`Finsupp.single i 1`. -/
 lemma toFinsupp_unitMono {k : ℕ} (i : Fin k) :
-    CMvMonomial.toFinsupp (Vector.ofFn (fun j : Fin k => if j = i then 1 else 0)) =
+    CMvMonomial.toFinsupp
+      (Vector.ofFn (fun j : Fin k =>
+        if j = i then 1 else 0)) =
     Finsupp.single i 1 := by
   ext j
-  simp [CMvMonomial.toFinsupp, Vector.get, Finsupp.single_apply, eq_comm]
+  simp [CMvMonomial.toFinsupp, Vector.get,
+    Finsupp.single_apply, eq_comm]
 
-/-- `fromCMvPolynomial` maps our `X i` to Mathlib's `X i`. -/
+/-- `fromCMvPolynomial` maps `CMvPolynomial.X i` to
+`MvPolynomial.X i`. -/
 lemma fromCMvPolynomial_X {k : ℕ} (i : Fin k) :
-    fromCMvPolynomial (CMvPolynomial.X (R := R) i) = MvPolynomial.X i := by
-  rw [X_eq_monomial, fromCMvPolynomial_monomial, toFinsupp_unitMono]
+    fromCMvPolynomial (CMvPolynomial.X (R := R) i) =
+    MvPolynomial.X i := by
+  rw [X_eq_monomial, fromCMvPolynomial_monomial,
+    toFinsupp_unitMono]
   rfl
 
 /-- Renaming maps variable `X i` to `X (f i)`. -/
 @[simp]
 lemma rename_X (f : Fin n → Fin m) (i : Fin n) :
-    CMvPolynomial.rename f (CMvPolynomial.X (R := R) i) = CMvPolynomial.X (f i) := by
+    CMvPolynomial.rename f (CMvPolynomial.X (R := R) i) =
+    CMvPolynomial.X (f i) := by
   apply fromCMvPolynomial_injective
-  rw [fromCMvPolynomial_rename, fromCMvPolynomial_X, fromCMvPolynomial_X]
+  rw [fromCMvPolynomial_rename, fromCMvPolynomial_X,
+    fromCMvPolynomial_X]
   exact MvPolynomial.rename_X f i
 
 /-- Renaming preserves addition. -/
 @[simp]
-lemma rename_add (f : Fin n → Fin m) (p q : CMvPolynomial n R) :
+lemma rename_add (f : Fin n → Fin m)
+    (p q : CMvPolynomial n R) :
     CMvPolynomial.rename f (p + q) =
-    CMvPolynomial.rename f p + CMvPolynomial.rename f q := by
+    CMvPolynomial.rename f p +
+    CMvPolynomial.rename f q := by
   apply fromCMvPolynomial_injective
   simp only [fromCMvPolynomial_rename, CPoly.map_add]
-  exact _root_.map_add (MvPolynomial.rename f) (fromCMvPolynomial p) (fromCMvPolynomial q)
+  exact _root_.map_add (MvPolynomial.rename f)
+    (fromCMvPolynomial p) (fromCMvPolynomial q)
 
 /-- Renaming preserves multiplication. -/
 @[simp]
-lemma rename_mul (f : Fin n → Fin m) (p q : CMvPolynomial n R) :
+lemma rename_mul (f : Fin n → Fin m)
+    (p q : CMvPolynomial n R) :
     CMvPolynomial.rename f (p * q) =
-    CMvPolynomial.rename f p * CMvPolynomial.rename f q := by
+    CMvPolynomial.rename f p *
+    CMvPolynomial.rename f q := by
   apply fromCMvPolynomial_injective
   simp only [fromCMvPolynomial_rename, CPoly.map_mul]
-  exact _root_.map_mul (MvPolynomial.rename f) (fromCMvPolynomial p) (fromCMvPolynomial q)
+  exact _root_.map_mul (MvPolynomial.rename f)
+    (fromCMvPolynomial p) (fromCMvPolynomial q)
 
 /-- Renaming by the identity function is the identity. -/
 @[simp]
@@ -249,23 +274,28 @@ lemma rename_id (p : CMvPolynomial n R) :
   rw [fromCMvPolynomial_rename]
   exact MvPolynomial.rename_id_apply (fromCMvPolynomial p)
 
-/-- Composing two renamings is the same as renaming by the composition. -/
+/-- Composing two renamings equals renaming by the composition. -/
 @[simp]
-lemma rename_rename {k : ℕ} (f : Fin n → Fin m) (g : Fin m → Fin k)
-    (p : CMvPolynomial n R) :
+lemma rename_rename {k : ℕ} (f : Fin n → Fin m)
+    (g : Fin m → Fin k) (p : CMvPolynomial n R) :
     CMvPolynomial.rename g (CMvPolynomial.rename f p) =
     CMvPolynomial.rename (g ∘ f) p := by
   apply fromCMvPolynomial_injective
-  rw [fromCMvPolynomial_rename, fromCMvPolynomial_rename, fromCMvPolynomial_rename]
+  rw [fromCMvPolynomial_rename, fromCMvPolynomial_rename,
+    fromCMvPolynomial_rename]
   exact MvPolynomial.rename_rename f g (fromCMvPolynomial p)
 
-/-- Ring equivalence for variable renaming when the function is a bijection. -/
-noncomputable def CMvPolynomial.renameEquiv (f : Fin n ≃ Fin m) :
+/-- Ring equivalence for variable renaming when the function is
+a bijection. -/
+noncomputable def CMvPolynomial.renameEquiv
+    (f : Fin n ≃ Fin m) :
     CMvPolynomial n R ≃+* CMvPolynomial m R where
   toFun := CMvPolynomial.rename f
   invFun := CMvPolynomial.rename f.symm
-  left_inv p := by rw [rename_rename, f.symm_comp_self, rename_id]
-  right_inv q := by rw [rename_rename, f.self_comp_symm, rename_id]
+  left_inv p := by
+    rw [rename_rename, f.symm_comp_self, rename_id]
+  right_inv q := by
+    rw [rename_rename, f.self_comp_symm, rename_id]
   map_add' p q := rename_add f p q
   map_mul' p q := rename_mul f p q
 

From ad4b9a4633eb9549b7452fc9b1a85635df7c737a Mon Sep 17 00:00:00 2001
From: Dimitris <di.mitsios@gmail.com>
Date: Fri, 13 Feb 2026 14:52:17 +0200
Subject: [PATCH 6/6] Authors field added

---
 CompPoly/Multivariate/Rename.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/CompPoly/Multivariate/Rename.lean b/CompPoly/Multivariate/Rename.lean
index 2d714c0..6be9efa 100644
--- a/CompPoly/Multivariate/Rename.lean
+++ b/CompPoly/Multivariate/Rename.lean
@@ -1,6 +1,7 @@
 /-
 Copyright (c) 2025 CompPoly. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Dimitris Mitsios
 -/
 import CompPoly.Multivariate.MvPolyEquiv
 import Mathlib.Algebra.MvPolynomial.Rename