diff --git a/Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean b/Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean
index ad4a97ace..583458750 100644
--- a/Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean
+++ b/Physlib/Relativity/Tensors/ComplexTensor/Vector/Pre/Basic.lean
@@ -194,7 +194,7 @@ lemma complexContrBasis_of_real (i : Fin 1 ⊕ Fin 3) :
 
 lemma inclCongrRealLorentz_ρ (M : SL(2, ℂ)) (v : ContrMod 3) :
     (ContrℂModule.SL2CRep M) (inclCongrRealLorentz v) =
-    inclCongrRealLorentz ((Contr 3).ρ (SL2C.toLorentzGroup M) v) := by
+    inclCongrRealLorentz (ContrMod.rep (SL2C.toLorentzGroup M) v) := by
   apply Lorentz.ContrℂModule.ext
   rw [complexContrBasis_ρ_val, inclCongrRealLorentz_val, inclCongrRealLorentz_val]
   rw [LorentzGroup.toComplex_mulVec_ofReal]
@@ -246,7 +246,7 @@ lemma complexCoBasis_of_real (i : Fin 1 ⊕ Fin 3) :
 
 lemma inclCoRealLorentz_ρ (M : SL(2, ℂ)) (v : CoMod 3) :
     (CoℂModule.SL2CRep M) (inclCoRealLorentz v) =
-    inclCoRealLorentz ((Co 3).ρ (SL2C.toLorentzGroup M) v) := by
+    inclCoRealLorentz (CoMod.rep (SL2C.toLorentzGroup M) v) := by
   ext i
   rw [CoℂModule.SL2CRep_val, inclCoRealLorentz_val, inclCoRealLorentz_val]
   change ((LorentzGroup.toComplex (SL2C.toLorentzGroup M))⁻¹ᵀ *ᵥ
diff --git a/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean b/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean
index bd205a693..7162b8956 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Matrix/Pre.lean
@@ -20,7 +20,7 @@ open Matrix Module MatrixGroups Complex TensorProduct CategoryTheory.MonoidalCat
 
 namespace Lorentz
 
-/-- Equivalence of `Contr ⊗ Contr` to `(1 + d) x (1 + d)` real matrices. -/
+/-- Equivalence of `ContrMod ⊗ ContrMod` to `(1 + d) x (1 + d)` real matrices. -/
 def contrContrToMatrixRe {d : ℕ} : (ContrMod d ⊗[ℝ] ContrMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (contrBasis d) (contrBasis d)).repr ≪≫ₗ
@@ -39,8 +39,8 @@ lemma contrContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1
     rfl
   · simp
 
-/-- Equivalence of `Co ⊗ Co` to `(1 + d) x (1 + d)` real matrices. -/
-def coCoToMatrixRe {d : ℕ} : (Co d ⊗ Co d).V ≃ₗ[ℝ]
+/-- Equivalence of `CoMod ⊗ CoMod` to `(1 + d) x (1 + d)` real matrices. -/
+def coCoToMatrixRe {d : ℕ} : (CoMod d ⊗[ℝ] CoMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (coBasis d) (coBasis d)).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ
@@ -57,8 +57,8 @@ lemma coCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ F
     rfl
   · simp
 
-/-- Equivalence of `Contr d ⊗ Co d` to `(1 + d) x (1 + d)` real matrices. -/
-def contrCoToMatrixRe {d : ℕ} : (Contr d ⊗ Co d).V ≃ₗ[ℝ]
+/-- Equivalence of `ContrMod d ⊗ CoMod d` to `(1 + d) x (1 + d)` real matrices. -/
+def contrCoToMatrixRe {d : ℕ} : (ContrMod d ⊗[ℝ] CoMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (contrBasis d) (coBasis d)).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ
@@ -76,8 +76,8 @@ lemma contrCoToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 
     rfl
   · simp
 
-/-- Equivalence of `Co d ⊗ Contr d` to `(1 + d) x (1 + d)` real matrices. -/
-def coContrToMatrixRe : (Co d ⊗ Contr d).V ≃ₗ[ℝ]
+/-- Equivalence of `CoMod d ⊗ ContrMod d` to `(1 + d) x (1 + d)` real matrices. -/
+def coContrToMatrixRe : (CoMod d ⊗[ℝ] ContrMod d) ≃ₗ[ℝ]
     Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ :=
   (Basis.tensorProduct (coBasis d) (contrBasis d)).repr ≪≫ₗ
   Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)) ≪≫ₗ
@@ -102,28 +102,28 @@ lemma coContrToMatrixRe_symm_expand_tmul (M : Matrix (Fin 1 ⊕ Fin d) (Fin 1 
 -/
 
 set_option backward.isDefEq.respectTransparency false in
-lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (Contr d ⊗ Contr d).V) (M : LorentzGroup d) :
-    contrContrToMatrixRe (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M) v) =
+lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (ContrMod d ⊗[ℝ] ContrMod d)) (M : LorentzGroup d) :
+    contrContrToMatrixRe (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M) v) =
     M.1 * contrContrToMatrixRe v * Mᵀ := by
   nth_rewrite 1 [contrContrToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((contrBasis d).tensorProduct (contrBasis d))
       ((contrBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)))
+      (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((contrBasis d).tensorProduct (contrBasis d)).repr v)))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((contrBasis d).tensorProduct (contrBasis d))
       ((contrBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)) v)
+      (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M))
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M)) (i, j) k)
         * contrContrToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -139,28 +139,28 @@ lemma contrContrToMatrixRe_ρ {d : ℕ} (v : (Contr d ⊗ Contr d).V) (M : Loren
   ring
 
 set_option backward.isDefEq.respectTransparency false in
-lemma coCoToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Co d)).V) (M : LorentzGroup d) :
-    coCoToMatrixRe (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M) v) =
+lemma coCoToMatrixRe_ρ {d : ℕ} (v : (CoMod d ⊗[ℝ] CoMod d)) (M : LorentzGroup d) :
+    coCoToMatrixRe (TensorProduct.map (CoMod.rep M) (CoMod.rep M) v) =
     M.1⁻¹ᵀ * coCoToMatrixRe v * M⁻¹ := by
   nth_rewrite 1 [coCoToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((coBasis d).tensorProduct (coBasis d))
       ((coBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M))
+      (TensorProduct.map (CoMod.rep M) (CoMod.rep M))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((coBasis d).tensorProduct (coBasis d)).repr v))))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((coBasis d).tensorProduct (coBasis d))
       ((coBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M)) v)
+      (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M))
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M)) (i, j) k)
         * coCoToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -176,28 +176,28 @@ lemma coCoToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Co d)).V) (M : LorentzGroup
   ring
 
 set_option backward.isDefEq.respectTransparency false in
-lemma contrCoToMatrixRe_ρ {d : ℕ} (v : ((Contr d) ⊗ (Co d)).V) (M : LorentzGroup d) :
-    contrCoToMatrixRe (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M) v) =
+lemma contrCoToMatrixRe_ρ {d : ℕ} (v : (ContrMod d ⊗[ℝ] CoMod d)) (M : LorentzGroup d) :
+    contrCoToMatrixRe (TensorProduct.map (ContrMod.rep M) (CoMod.rep M) v) =
     M.1 * contrCoToMatrixRe v * M.1⁻¹ := by
   nth_rewrite 1 [contrCoToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((contrBasis d).tensorProduct (coBasis d))
       ((contrBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M))
+      (TensorProduct.map (ContrMod.rep M) (CoMod.rep M))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((contrBasis d).tensorProduct (coBasis d)).repr v))))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((contrBasis d).tensorProduct (coBasis d))
       ((contrBasis d).tensorProduct (coBasis d))
-      (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M)) v)
+      (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M))
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M))
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M)) (i, j) k)
         * contrCoToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply]
@@ -213,28 +213,28 @@ lemma contrCoToMatrixRe_ρ {d : ℕ} (v : ((Contr d) ⊗ (Co d)).V) (M : Lorentz
   ring
 
 set_option backward.isDefEq.respectTransparency false in
-lemma coContrToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Contr d)).V) (M : LorentzGroup d) :
-    coContrToMatrixRe (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M) v) =
+lemma coContrToMatrixRe_ρ {d : ℕ} (v : (CoMod d ⊗[ℝ] ContrMod d)) (M : LorentzGroup d) :
+    coContrToMatrixRe (TensorProduct.map (CoMod.rep M) (ContrMod.rep M) v) =
     M.1⁻¹ᵀ * coContrToMatrixRe v * M.1ᵀ := by
   nth_rewrite 1 [coContrToMatrixRe]
   simp only [LinearEquiv.trans_apply]
   trans (LinearEquiv.curry ℝ ℝ (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d)) ((LinearMap.toMatrix
       ((coBasis d).tensorProduct (contrBasis d))
       ((coBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M))
+      (TensorProduct.map (CoMod.rep M) (ContrMod.rep M))
       *ᵥ ((Finsupp.linearEquivFunOnFinite ℝ ℝ ((Fin 1 ⊕ Fin d) × (Fin 1 ⊕ Fin d)))
       (((coBasis d).tensorProduct (contrBasis d)).repr v))))
   · apply congrArg
     have h1 := (LinearMap.toMatrix_mulVec_repr ((coBasis d).tensorProduct (contrBasis d))
       ((coBasis d).tensorProduct (contrBasis d))
-      (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M)) v)
+      (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) v)
     erw [h1]
     rfl
   rw [TensorProduct.toMatrix_map]
   funext i j
   change ∑ k, ((kroneckerMap (fun x1 x2 => x1 * x2)
-        ((LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M))
-        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M)) (i, j) k)
+        ((LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M))
+        ((LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M)) (i, j) k)
         * coContrToMatrixRe v k.1 k.2) = _
   rw [Fintype.sum_prod_type]
   simp_rw [kroneckerMap_apply, Matrix.mul_apply, Matrix.transpose_apply]
@@ -257,14 +257,14 @@ lemma coContrToMatrixRe_ρ {d : ℕ} (v : ((Co d) ⊗ (Contr d)).V) (M : Lorentz
 
 lemma contrContrToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M) (contrContrToMatrixRe.symm v) =
+    TensorProduct.map (ContrMod.rep M) (ContrMod.rep M) (contrContrToMatrixRe.symm v) =
     contrContrToMatrixRe.symm (M.1 * v * M.1ᵀ) := by
   refine contrContrToMatrixRe.injective ?_
   simp [contrContrToMatrixRe_ρ]
 
 lemma coCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Co d).ρ M) ((Co d).ρ M) (coCoToMatrixRe.symm v) =
+    TensorProduct.map (CoMod.rep M) (CoMod.rep M) (coCoToMatrixRe.symm v) =
     coCoToMatrixRe.symm (M.1⁻¹ᵀ * v * M.1⁻¹) := by
   have h1 := coCoToMatrixRe_ρ (coCoToMatrixRe.symm v) M
   simp only [LinearEquiv.apply_symm_apply, ← LorentzGroup.coe_inv] at h1
@@ -274,7 +274,7 @@ lemma coCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕
 
 lemma contrCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M) (contrCoToMatrixRe.symm v) =
+    TensorProduct.map (ContrMod.rep M) (CoMod.rep M) (contrCoToMatrixRe.symm v) =
     contrCoToMatrixRe.symm (M.1 * v * M.1⁻¹) := by
   have h1 := contrCoToMatrixRe_ρ (contrCoToMatrixRe.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
@@ -282,7 +282,7 @@ lemma contrCoToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 
 
 lemma coContrToMatrixRe_ρ_symm {d : ℕ} (v : Matrix (Fin 1 ⊕ Fin d) (Fin 1 ⊕ Fin d) ℝ)
     (M : LorentzGroup d) :
-    TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M) (coContrToMatrixRe.symm v) =
+    TensorProduct.map (CoMod.rep M) (ContrMod.rep M) (coContrToMatrixRe.symm v) =
     coContrToMatrixRe.symm (M.1⁻¹ᵀ * v * M.1ᵀ) := by
   have h1 := coContrToMatrixRe_ρ (coContrToMatrixRe.symm v) M
   simp only [LinearEquiv.apply_symm_apply] at h1
diff --git a/Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean b/Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean
index e10b41dcb..d346da31b 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Metrics/Pre.lean
@@ -20,7 +20,7 @@ open Module Matrix MatrixGroups Complex TensorProduct CategoryTheory.MonoidalCat
 namespace Lorentz
 open scoped TensorProduct
 
-/-- The metric `ηᵃᵃ` as an element of `(Contr d ⊗ Contr d).V`. -/
+/-- The metric `ηᵃᵃ` as an element of `(ContrMod d ⊗[ℝ] ContrMod d)`. -/
 def preContrMetricVal (d : ℕ := 3) : ContrMod d ⊗[ℝ] ContrMod d :=
   contrContrToMatrixRe.symm ((@minkowskiMatrix d))
 
@@ -39,7 +39,7 @@ lemma preContrMetricVal_expand_tmul {d : ℕ} : preContrMetricVal d =
     sub_eq_add_neg]
 
 set_option backward.isDefEq.respectTransparency false in
-/-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ Contr d ⊗ Contr d`,
+/-- The metric `ηᵃᵃ` as a morphism `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ ContrMod.rep ⊗ ContrMod.rep`,
   making its invariance under the action of `LorentzGroup d`. -/
 def preContrMetric (d : ℕ := 3) :
     (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
@@ -51,7 +51,7 @@ def preContrMetric (d : ℕ := 3) :
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • (preContrMetricVal d) =
-      (TensorProduct.map ((Contr d).ρ M) ((Contr d).ρ M)) (x • (preContrMetricVal d))
+      (TensorProduct.map (ContrMod.rep M) (ContrMod.rep M)) (x • (preContrMetricVal d))
     simp only [map_smul]
     apply congrArg
     simp only [preContrMetricVal]
@@ -63,8 +63,8 @@ def preContrMetric (d : ℕ := 3) :
 lemma preContrMetric_apply_one {d : ℕ} : (preContrMetric d) (1 : ℝ) = preContrMetricVal d :=
   one_smul ℝ _
 
-/-- The metric `ηᵢᵢ` as an element of `(Co d ⊗ Co d).V`. -/
-def preCoMetricVal (d : ℕ := 3) : (Co d ⊗ Co d).V :=
+/-- The metric `ηᵢᵢ` as an element of `(CoMod d ⊗[ℝ] CoMod d)`. -/
+def preCoMetricVal (d : ℕ := 3) : CoMod d ⊗[ℝ] CoMod d :=
   coCoToMatrixRe.symm ((@minkowskiMatrix d))
 
 lemma preCoMetricVal_expand_tmul_minkowskiMatrix {d : ℕ} : preCoMetricVal d =
@@ -82,7 +82,7 @@ lemma preCoMetricVal_expand_tmul {d : ℕ} : preCoMetricVal d =
     sub_eq_add_neg]
 
 set_option backward.isDefEq.respectTransparency false in
-/-- The metric `ηᵢᵢ` as a morphism `𝟙_ (Rep ℂ (LorentzGroup d))) ⟶ Co d ⊗ Co d`,
+/-- The metric `ηᵢᵢ` as a morphism `𝟙_ (Rep ℂ (LorentzGroup d))) ⟶ CoMod.rep ⊗ CoMod.rep`,
   making its invariance under the action of `LorentzGroup d`. -/
 def preCoMetric (d : ℕ := 3) : (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
     ((CoMod.rep).tprod (CoMod.rep)) where
@@ -93,7 +93,7 @@ def preCoMetric (d : ℕ := 3) : (Representation.trivial ℝ (LorentzGroup d) 
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • preCoMetricVal d =
-      (TensorProduct.map ((Co d).ρ M) ((Co d).ρ M)) (x • preCoMetricVal d)
+      (TensorProduct.map (CoMod.rep M) (CoMod.rep M)) (x • preCoMetricVal d)
     simp only [_root_.map_smul]
     apply congrArg
     simp only [preCoMetricVal]
diff --git a/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean b/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
index 3a1dfb51d..8ce430965 100644
--- a/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/ToComplex.lean
@@ -472,7 +472,7 @@ lemma actionP_toComplexPure {n : ℕ} (c : Fin n → Color) (p : Pure realLorent
           = (Lorentz.ContrℂModule.SL2CRep Λ) (Lorentz.inclCongrRealLorentz p) := by
             exact congrArg (Lorentz.ContrℂModule.SL2CRep Λ)
               (toComplexVector_up_eq_inclCongrRealLorentz p)
-      _ = Lorentz.inclCongrRealLorentz ((Lorentz.Contr 3).ρ (toLorentzGroup Λ) p) := by
+      _ = Lorentz.inclCongrRealLorentz (Lorentz.ContrMod.rep (toLorentzGroup Λ) p) := by
         rw [Lorentz.inclCongrRealLorentz_ρ]
       _ = (toComplexVector Color.up) ((Lorentz.ContrMod.rep (toLorentzGroup Λ)) p) := by
         exact (toComplexVector_up_eq_inclCongrRealLorentz
@@ -483,7 +483,7 @@ lemma actionP_toComplexPure {n : ℕ} (c : Fin n → Color) (p : Pure realLorent
           = (Lorentz.CoℂModule.SL2CRep Λ) (Lorentz.inclCoRealLorentz p) := by
             exact congrArg (Lorentz.CoℂModule.SL2CRep Λ)
               (toComplexVector_down_eq_inclCoRealLorentz p)
-      _ = Lorentz.inclCoRealLorentz ((Lorentz.Co 3).ρ (toLorentzGroup Λ) p) := by
+      _ = Lorentz.inclCoRealLorentz (Lorentz.CoMod.rep (toLorentzGroup Λ) p) := by
         rw [Lorentz.inclCoRealLorentz_ρ]
       _ = (toComplexVector Color.down) ((Lorentz.CoMod.rep (toLorentzGroup Λ)) p) := by
         exact (toComplexVector_down_eq_inclCoRealLorentz
diff --git a/Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean b/Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean
index fc510c0bb..605ae3f2c 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Units/Pre.lean
@@ -21,7 +21,7 @@ open Module Matrix MatrixGroups Complex TensorProduct CategoryTheory.MonoidalCat
 namespace Lorentz
 
 /-- The contra-co unit for complex lorentz vectors. Usually denoted `δⁱᵢ`. -/
-def preContrCoUnitVal (d : ℕ := 3) : (Contr d ⊗ Co d).V :=
+def preContrCoUnitVal (d : ℕ := 3) : ContrMod d ⊗[ℝ] CoMod d :=
   contrCoToMatrixRe.symm 1
 
 /-- Expansion of `preContrCoUnitVal` into basis. -/
@@ -60,7 +60,7 @@ def preContrCoUnit (d : ℕ := 3) :
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • preContrCoUnitVal d =
-      (TensorProduct.map ((Contr d).ρ M) ((Co d).ρ M)) (x • preContrCoUnitVal d)
+      (TensorProduct.map (ContrMod.rep M) (CoMod.rep M)) (x • preContrCoUnitVal d)
     simp only [map_smul]
     apply congrArg
     simp only [preContrCoUnitVal]
@@ -73,7 +73,7 @@ lemma preContrCoUnit_apply_one {d : ℕ} : (preContrCoUnit d) (1 : ℝ) = preCon
   rw [one_smul]
 
 /-- The co-contra unit for complex lorentz vectors. Usually denoted `δᵢⁱ`. -/
-def preCoContrUnitVal (d : ℕ := 3) : (Co d ⊗ Contr d).V :=
+def preCoContrUnitVal (d : ℕ := 3) : CoMod d ⊗[ℝ] ContrMod d :=
   coContrToMatrixRe.symm 1
 
 /-- Expansion of `preCoContrUnitVal` into basis. -/
@@ -97,7 +97,7 @@ lemma preCoContrUnitVal_expand_tmul {d : ℕ} : preCoContrUnitVal d =
 
 set_option backward.isDefEq.respectTransparency false in
 /-- The co-contra unit for complex lorentz vectors as a morphism
-  `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ Co d ⊗ Contr d`, manifesting the invariance under
+  `𝟙_ (Rep ℝ (LorentzGroup d)) ⟶ CoMod.rep ⊗ ContrMod.rep`, manifesting the invariance under
   the `LorentzGroup d` action. -/
 def preCoContrUnit (d : ℕ) : (Representation.trivial ℝ (LorentzGroup d) ℝ).IntertwiningMap
     ((CoMod.rep).tprod (ContrMod.rep)) where
@@ -111,7 +111,7 @@ def preCoContrUnit (d : ℕ) : (Representation.trivial ℝ (LorentzGroup d) ℝ)
     refine LinearMap.ext fun x : ℝ => ?_
     simp only [LinearMap.coe_comp, Function.comp_apply]
     change x • preCoContrUnitVal d =
-      (TensorProduct.map ((Co d).ρ M) ((Contr d).ρ M)) (x • preCoContrUnitVal d)
+      (TensorProduct.map (CoMod.rep M) (ContrMod.rep M)) (x • preCoContrUnitVal d)
     simp only [map_smul]
     apply congrArg
     simp only [preCoContrUnitVal]
diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean
index 182087ea6..f2f6c988c 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Basic.lean
@@ -23,12 +23,6 @@ open Matrix Module MatrixGroups Complex TensorProduct
 
 namespace Lorentz
 open minkowskiMatrix
-/-- The representation of `LorentzGroup d` on real vectors corresponding to contravariant
-  Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
-def Contr (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of ContrMod.rep
-
-TODO "The definition of `Contr` can be removed and everywhere replaced with `ContrMod.rep`.
-  Similar for `Co` and `CoMod.rep`."
 
 /-- The standard basis of contravariant Lorentz vectors. -/
 def contrBasis (d : ℕ := 3) : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) :=
@@ -36,7 +30,7 @@ def contrBasis (d : ℕ := 3) : Basis (Fin 1 ⊕ Fin d) ℝ (ContrMod d) :=
 
 @[simp]
 lemma contrBasis_ρ_apply {d : ℕ} (M : LorentzGroup d) (i j : Fin 1 ⊕ Fin d) :
-    (LinearMap.toMatrix (contrBasis d) (contrBasis d)) ((Contr d).ρ M) i j =
+    (LinearMap.toMatrix (contrBasis d) (contrBasis d)) (ContrMod.rep M) i j =
     M.1 i j := by
   rw [LinearMap.toMatrix_apply]
   simp only [contrBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply]
@@ -49,7 +43,7 @@ lemma contrBasis_toFin1dℝ {d : ℕ} (i : Fin 1 ⊕ Fin d) :
   simp only [ContrMod.toFin1dℝ, contrBasis, Basis.coe_ofEquivFun]
   rfl
 
-lemma contrBasis_repr_apply {d : ℕ} (p : Contr d) (i : Fin 1 ⊕ Fin d) :
+lemma contrBasis_repr_apply {d : ℕ} (p : ContrMod d) (i : Fin 1 ⊕ Fin d) :
     (contrBasis d).repr p i = p.val i := by
   simp only [contrBasis, Basis.ofEquivFun_repr_apply]
   rfl
@@ -66,41 +60,32 @@ lemma contrBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
 lemma contrBasisFin_repr_apply {d : ℕ} (p : ContrMod d) (i : Fin (1 + d)) :
     (contrBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := by rfl
 
-/-- The representation of contravariant Lorentz vectors forms a topological space, induced
-  by its equivalence to `Fin 1 ⊕ Fin d → ℝ`. -/
-instance : TopologicalSpace (Contr d) := TopologicalSpace.induced
-  ContrMod.toFin1dℝEquiv (Pi.topologicalSpace)
-
-lemma continuous_contr {T : Type} [TopologicalSpace T] (f : T → Contr d)
+lemma continuous_contr {T : Type} [TopologicalSpace T] (f : T → ContrMod d)
     (h : Continuous (fun i => (f i).toFin1dℝ)) : Continuous f := by
   exact continuous_induced_rng.mpr h
 
 set_option backward.isDefEq.respectTransparency false in
-lemma contr_continuous {T : Type} [TopologicalSpace T] (f : Contr d → T)
+lemma contr_continuous {T : Type} [TopologicalSpace T] (f : ContrMod d → T)
     (h : Continuous (f ∘ (@ContrMod.toFin1dℝEquiv d).symm)) : Continuous f := by
   let x := Equiv.toHomeomorphOfIsInducing (@ContrMod.toFin1dℝEquiv d).toEquiv
     ContrMod.toFin1dℝEquiv_isInducing
   rw [← Homeomorph.comp_continuous_iff' x.symm]
   exact h
 
-/-- The representation of `LorentzGroup d` on real vectors corresponding to covariant
-  Lorentz vectors. In index notation these have an up index `ψⁱ`. -/
-def Co (d : ℕ) : Rep ℝ (LorentzGroup d) := Rep.of CoMod.rep
-
 /-- The standard basis of contravariant Lorentz vectors. -/
 def coBasis (d : ℕ := 3) : Basis (Fin 1 ⊕ Fin d) ℝ (CoMod d) :=
   Basis.ofEquivFun CoMod.toFin1dℝEquiv
 
 @[simp]
 lemma coBasis_ρ_apply {d : ℕ} (M : LorentzGroup d) (i j : Fin 1 ⊕ Fin d) :
-    (LinearMap.toMatrix (coBasis d) (coBasis d)) ((Co d).ρ M) i j =
+    (LinearMap.toMatrix (coBasis d) (coBasis d)) (CoMod.rep M) i j =
     M⁻¹ᵀ i j := by
   rw [LinearMap.toMatrix_apply]
   simp only [coBasis, Basis.coe_ofEquivFun, Basis.ofEquivFun_repr_apply, transpose_apply]
   change (_ *ᵥ (Pi.single j 1)) i = _
   simp [LorentzGroup.transpose, ← LorentzGroup.coe_inv]
 
-lemma coBasis_repr_apply {d : ℕ} (p : Co d) (i : Fin 1 ⊕ Fin d) :
+lemma coBasis_repr_apply {d : ℕ} (p : CoMod d) (i : Fin 1 ⊕ Fin d) :
     (coBasis d).repr p i = p.val i := by
   simp only [coBasis, Basis.ofEquivFun_repr_apply]
   rfl
@@ -120,7 +105,7 @@ lemma coBasisFin_toFin1dℝ {d : ℕ} (i : Fin (1 + d)) :
     (coBasisFin d i).toFin1dℝ = Pi.single (finSumFinEquiv.symm i) 1 := by
   simp only [coBasisFin, Basis.reindex_apply, coBasis_toFin1dℝ]
 
-lemma coBasisFin_repr_apply {d : ℕ} (p : Co d) (i : Fin (1 + d)) :
+lemma coBasisFin_repr_apply {d : ℕ} (p : CoMod d) (i : Fin (1 + d)) :
     (coBasisFin d).repr p i = p.val (finSumFinEquiv.symm i) := by rfl
 
 open CategoryTheory.MonoidalCategory
@@ -132,7 +117,7 @@ open CategoryTheory.MonoidalCategory
 -/
 
 open Representation
-/-- The morphism of representations from `Contr d` to `Co d` defined by multiplication
+/-- The morphism of representations from `ContrMod.rep` to `CoMod.rep` defined by multiplication
   with the metric. -/
 def Contr.toCo (d : ℕ) : IntertwiningMap (ContrMod.rep (d := d)) (CoMod.rep (d := d)) where
   toFun := fun ψ => CoMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)
@@ -149,7 +134,7 @@ def Contr.toCo (d : ℕ) : IntertwiningMap (ContrMod.rep (d := d)) (CoMod.rep (d
       rw [mulVec_mulVec, LorentzGroup.minkowskiMatrix_comm, ← mulVec_mulVec]
     rfl
 
-/-- The morphism of representations from `Co d` to `Contr d` defined by multiplication
+/-- The morphism of representations from `CoMod.rep` to `ContrMod.rep` defined by multiplication
   with the metric. -/
 def Co.toContr (d : ℕ) : IntertwiningMap (CoMod.rep (d := d)) (ContrMod.rep (d := d)) where
     toFun := fun ψ => ContrMod.toFin1dℝEquiv.symm (η *ᵥ ψ.toFin1dℝ)
@@ -166,7 +151,7 @@ def Co.toContr (d : ℕ) : IntertwiningMap (CoMod.rep (d := d)) (ContrMod.rep (d
         rw [mulVec_mulVec, ← LorentzGroup.comm_minkowskiMatrix, ← mulVec_mulVec]
       rfl
 
-/-- The isomorphism between `Contr d` and `Co d` induced by multiplication with the
+/-- The isomorphism between `ContrMod.rep` and `CoMod.rep` induced by multiplication with the
   Minkowski metric. -/
 def contrIsoCo (d : ℕ) : Representation.Equiv (ContrMod.rep (d := d)) (CoMod.rep (d := d)) := by
   refine Representation.Equiv.mk' (Contr.toCo d) (Co.toContr d) ?_ ?_
@@ -184,7 +169,7 @@ namespace Contr
 
 open Lorentz
 lemma ρ_stdBasis (μ : Fin 1 ⊕ Fin 3) (Λ : LorentzGroup 3) :
-    (Contr 3).ρ Λ (ContrMod.stdBasis μ) = ∑ j, Λ.1 j μ • ContrMod.stdBasis j := by
+    ContrMod.rep Λ (ContrMod.stdBasis μ) = ∑ j, Λ.1 j μ • ContrMod.stdBasis j := by
   change Λ *ᵥ ContrMod.stdBasis μ = ∑ j, Λ.1 j μ • ContrMod.stdBasis j
   apply ContrMod.ext
   simp only [toLinAlgEquiv_self, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
diff --git a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean
index 48354dbc7..1d82b73a5 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Vector/Pre/Contraction.lean
@@ -75,7 +75,7 @@ def coModContrModBi (d : ℕ) : CoMod d →ₗ[ℝ] ContrMod d →ₗ[ℝ] ℝ w
     rw [smul_dotProduct]
     rfl
 
-/-- The linear map from Contr d ⊗ Co d to ℝ given by
+/-- The linear map from ContrMod d ⊗ CoMod d to ℝ given by
     summing over components of contravariant Lorentz vector and
     covariant Lorentz vector in the
     standard basis (i.e. the dot product).
@@ -97,10 +97,11 @@ def contrCoContract : ((ContrMod.rep).tprod (CoMod.rep)).IntertwiningMap
 /-- Notation for `contrCoContract` acting on a tmul. -/
 local notation "⟪" ψ "," φ "⟫ₘ" => contrCoContract (ψ ⊗ₜ φ)
 
-lemma contrCoContract_hom_tmul (ψ : Contr d) (φ : Co d) : ⟪ψ, φ⟫ₘ = ψ.toFin1dℝ ⬝ᵥ φ.toFin1dℝ := by
+lemma contrCoContract_hom_tmul (ψ : ContrMod d) (φ : CoMod d) :
+    ⟪ψ, φ⟫ₘ = ψ.toFin1dℝ ⬝ᵥ φ.toFin1dℝ := by
   rfl
 
-/-- The linear map from Co d ⊗ Contr d to ℝ given by
+/-- The linear map from CoMod d ⊗ ContrMod d to ℝ given by
     summing over components of contravariant Lorentz vector and
     covariant Lorentz vector in the
     standard basis (i.e. the dot product).
@@ -119,7 +120,8 @@ def coContrContract : ((CoMod.rep (d := d)).tprod (ContrMod.rep (d := d))).Inter
 /-- Notation for `coContrContract` acting on a tmul. -/
 local notation "⟪" φ "," ψ "⟫ₘ" => coContrContract (φ ⊗ₜ ψ)
 
-lemma coContrContract_hom_tmul (φ : Co d) (ψ : Contr d) : ⟪φ, ψ⟫ₘ = φ.toFin1dℝ ⬝ᵥ ψ.toFin1dℝ := by
+lemma coContrContract_hom_tmul (φ : CoMod d) (ψ : ContrMod d) :
+    ⟪φ, ψ⟫ₘ = φ.toFin1dℝ ⬝ᵥ ψ.toFin1dℝ := by
   rfl
 
 /-!
@@ -128,10 +130,10 @@ lemma coContrContract_hom_tmul (φ : Co d) (ψ : Contr d) : ⟪φ, ψ⟫ₘ = φ
 
 -/
 
-lemma contrCoContract_tmul_symm (φ : Contr d) (ψ : Co d) : ⟪φ, ψ⟫ₘ = ⟪ψ, φ⟫ₘ := by
+lemma contrCoContract_tmul_symm (φ : ContrMod d) (ψ : CoMod d) : ⟪φ, ψ⟫ₘ = ⟪ψ, φ⟫ₘ := by
   rw [contrCoContract_hom_tmul, coContrContract_hom_tmul, dotProduct_comm]
 
-lemma coContrContract_tmul_symm (φ : Co d) (ψ : Contr d) : ⟪φ, ψ⟫ₘ = ⟪ψ, φ⟫ₘ := by
+lemma coContrContract_tmul_symm (φ : CoMod d) (ψ : ContrMod d) : ⟪φ, ψ⟫ₘ = ⟪ψ, φ⟫ₘ := by
   rw [contrCoContract_tmul_symm]
 
 /-!
@@ -142,27 +144,27 @@ lemma coContrContract_tmul_symm (φ : Co d) (ψ : Contr d) : ⟪φ, ψ⟫ₘ = 
 open CategoryTheory.MonoidalCategory
 open CategoryTheory
 
-/-- The linear map from Contr d ⊗ Contr d to ℝ induced by the homomorphism
+/-- The linear map from ContrMod d ⊗ ContrMod d to ℝ induced by the homomorphism
   `Contr.toCo` and the contraction `contrCoContract`. -/
 def contrContrContract : ((ContrMod.rep (d := d)).tprod (ContrMod.rep (d := d))).IntertwiningMap
     (Representation.trivial ℝ (LorentzGroup d) ℝ) := contrCoContract.comp
   ((Contr.toCo d).lTensor (ContrMod.rep (d := d)))
 
-/-- The linear map from Contr d ⊗ Contr d to ℝ induced by the homomorphism
+/-- The linear map from ContrMod d ⊗ ContrMod d to ℝ induced by the homomorphism
   `Contr.toCo` and the contraction `contrCoContract`. -/
-def contrContrContractField : (Contr d).V ⊗[ℝ] (Contr d).V →ₗ[ℝ] ℝ :=
+def contrContrContractField : ContrMod d ⊗[ℝ] ContrMod d →ₗ[ℝ] ℝ :=
   contrContrContract.toLinearMap
 
 /-- Notation for `contrContrContractField` acting on a tmul. -/
 local notation "⟪" ψ "," φ "⟫ₘ" => contrContrContractField (ψ ⊗ₜ φ)
 
-lemma contrContrContract_hom_tmul (φ : Contr d) (ψ : Contr d) :
+lemma contrContrContract_hom_tmul (φ : ContrMod d) (ψ : ContrMod d) :
     ⟪φ, ψ⟫ₘ = φ.toFin1dℝ ⬝ᵥ η *ᵥ ψ.toFin1dℝ:= by
   simp only [contrContrContractField]
   erw [contrCoContract_hom_tmul]
   rfl
 
-/-- The linear map from Co d ⊗ Co d to ℝ induced by the homomorphism
+/-- The linear map from CoMod d ⊗ CoMod d to ℝ induced by the homomorphism
   `Co.toContr` and the contraction `coContrContract`. -/
 def coCoContract : ((CoMod.rep (d := d)).tprod (CoMod.rep (d := d))).IntertwiningMap
     (Representation.trivial ℝ (LorentzGroup d) ℝ) := coContrContract.comp
@@ -171,7 +173,7 @@ def coCoContract : ((CoMod.rep (d := d)).tprod (CoMod.rep (d := d))).Intertwinin
 /-- Notation for `coCoContract` acting on a tmul. -/
 local notation "⟪" ψ "," φ "⟫ₘ" => coCoContract (ψ ⊗ₜ φ)
 
-lemma coCoContract_hom_tmul (φ : Co d) (ψ : Co d) :
+lemma coCoContract_hom_tmul (φ : CoMod d) (ψ : CoMod d) :
     ⟪φ, ψ⟫ₘ = φ.toFin1dℝ ⬝ᵥ η *ᵥ ψ.toFin1dℝ := by rfl
 
 /-!
@@ -183,10 +185,10 @@ We derive the lemmas in main for `contrContrContractField`.
 -/
 namespace contrContrContractField
 
-variable (x y : Contr d)
+variable (x y : ContrMod d)
 
 @[simp]
-lemma action_tmul (g : LorentzGroup d) : ⟪(Contr d).ρ g x, (Contr d).ρ g y⟫ₘ = ⟪x, y⟫ₘ :=
+lemma action_tmul (g : LorentzGroup d) : ⟪ContrMod.rep g x, ContrMod.rep g y⟫ₘ = ⟪x, y⟫ₘ :=
   LinearMap.congr_fun (contrContrContract.isIntertwining' g) (x ⊗ₜ[ℝ] y)
 
 lemma as_sum : ⟪x, y⟫ₘ = x.val (Sum.inl 0) * y.val (Sum.inl 0) -
@@ -236,12 +238,12 @@ lemma dual_mulVec_right : ⟪x, dual Λ *ᵥ y⟫ₘ = ⟪Λ *ᵥ x, y⟫ₘ :=
 lemma dual_mulVec_left : ⟪dual Λ *ᵥ x, y⟫ₘ = ⟪x, Λ *ᵥ y⟫ₘ := by
   rw [symm, dual_mulVec_right, symm]
 
-lemma right_parity : ⟪x, (Contr d).ρ LorentzGroup.parity y⟫ₘ = ∑ i, x.val i * y.val i := by
+lemma right_parity : ⟪x, ContrMod.rep LorentzGroup.parity y⟫ₘ = ∑ i, x.val i * y.val i := by
   rw [as_sum]
   simp only [Fin.isValue, Fintype.sum_sum_type, Finset.univ_unique, Fin.default_eq_zero,
     Finset.sum_singleton]
-  trans x.val (Sum.inl 0) * (((Contr d).ρ LorentzGroup.parity) y).val (Sum.inl 0) +
-    ∑ i : Fin d, - (x.val (Sum.inr i) * (((Contr d).ρ LorentzGroup.parity) y).val (Sum.inr i))
+  trans x.val (Sum.inl 0) * ((ContrMod.rep LorentzGroup.parity) y).val (Sum.inl 0) +
+    ∑ i : Fin d, - (x.val (Sum.inr i) * ((ContrMod.rep LorentzGroup.parity) y).val (Sum.inr i))
   · simp only [Fin.isValue, Finset.sum_neg_distrib]
     rfl
   congr 1
@@ -254,7 +256,7 @@ lemma right_parity : ⟪x, (Contr d).ρ LorentzGroup.parity y⟫ₘ = ∑ i, x.v
     simp only [mulVec_inr_i, mul_neg, neg_neg, mul_eq_mul_left_iff]
     exact mul_eq_mul_left_iff.mp rfl
 
-lemma self_parity_eq_zero_iff : ⟪y, (Contr d).ρ LorentzGroup.parity y⟫ₘ = 0 ↔ y = 0 := by
+lemma self_parity_eq_zero_iff : ⟪y, ContrMod.rep LorentzGroup.parity y⟫ₘ = 0 ↔ y = 0 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · rw [right_parity] at h
     have hn := Fintype.sum_eq_zero_iff_of_nonneg (f := fun i => y.val i * y.val i) (fun i => by
@@ -271,7 +273,7 @@ lemma self_parity_eq_zero_iff : ⟪y, (Contr d).ρ LorentzGroup.parity y⟫ₘ =
     simp only [map_zero, tmul_zero]
 
 /-- The metric tensor is non-degenerate. -/
-lemma nondegenerate : (∀ (x : Contr d), ⟪x, y⟫ₘ = 0) ↔ y = 0 := by
+lemma nondegenerate : (∀ (x : ContrMod d), ⟪x, y⟫ₘ = 0) ↔ y = 0 := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · exact (self_parity_eq_zero_iff _).mp ((symm _ _).trans $ h _)
   · simp [h]
@@ -280,8 +282,8 @@ set_option backward.isDefEq.respectTransparency false in
 lemma matrix_apply_eq_iff_sub : ⟪x, Λ *ᵥ y⟫ₘ = ⟪x, Λ' *ᵥ y⟫ₘ ↔ ⟪x, (Λ - Λ') *ᵥ y⟫ₘ = 0 := by
   rw [← sub_eq_zero, ← LinearMap.map_sub, ← tmul_sub, ← ContrMod.sub_mulVec Λ Λ' y]
 
-lemma matrix_eq_iff_eq_forall' : (∀ (v : Contr d), (Λ *ᵥ v) = Λ' *ᵥ v) ↔
-    ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
+lemma matrix_eq_iff_eq_forall' : (∀ (v : ContrMod d), (Λ *ᵥ v) = Λ' *ᵥ v) ↔
+    ∀ (w v : ContrMod d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
   refine Iff.intro (fun h ↦ fun w v ↦ ?_) (fun h ↦ fun v ↦ ?_)
   · rw [h w]
   · simp only [matrix_apply_eq_iff_sub] at h
@@ -291,7 +293,7 @@ lemma matrix_eq_iff_eq_forall' : (∀ (v : Contr d), (Λ *ᵥ v) = Λ' *ᵥ v) 
     simp only [ContrMod.sub_mulVec] at h1
     exact h1
 
-lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
+lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ (w v : ContrMod d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, Λ' *ᵥ w⟫ₘ := by
   rw [← matrix_eq_iff_eq_forall']
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · subst h
@@ -300,12 +302,12 @@ lemma matrix_eq_iff_eq_forall : Λ = Λ' ↔ ∀ (w v : Contr d), ⟪v, Λ *ᵥ
     ext1 v
     exact h v
 
-lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ (w v : Contr d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
+lemma matrix_eq_id_iff : Λ = 1 ↔ ∀ (w v : ContrMod d), ⟪v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
   rw [matrix_eq_iff_eq_forall]
   simp only [ContrMod.one_mulVec]
 
 lemma _root_.LorentzGroup.mem_iff_invariant : Λ ∈ LorentzGroup d ↔
-    ∀ (w v : Contr d), ⟪Λ *ᵥ v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
+    ∀ (w v : ContrMod d), ⟪Λ *ᵥ v, Λ *ᵥ w⟫ₘ = ⟪v, w⟫ₘ := by
   refine Iff.intro (fun h => ?_) (fun h => ?_)
   · intro x y
     rw [← dual_mulVec_right, ContrMod.mulVec_mulVec]
@@ -320,7 +322,7 @@ lemma _root_.LorentzGroup.mem_iff_invariant : Λ ∈ LorentzGroup d ↔
 
 set_option backward.isDefEq.respectTransparency false in
 lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
-    ∀ (w : Contr d), ⟪Λ *ᵥ w, Λ *ᵥ w⟫ₘ = ⟪w, w⟫ₘ := by
+    ∀ (w : ContrMod d), ⟪Λ *ᵥ w, Λ *ᵥ w⟫ₘ = ⟪w, w⟫ₘ := by
   rw [LorentzGroup.mem_iff_invariant]
   refine Iff.intro (fun h x => h x x) (fun h x y => ?_)
   have hp := h (x + y)
@@ -345,7 +347,7 @@ lemma _root_.LorentzGroup.mem_iff_norm : Λ ∈ LorentzGroup d ↔
 
 -/
 
-lemma inl_sq_eq (v : Contr d) : v.val (Sum.inl 0) ^ 2 =
+lemma inl_sq_eq (v : ContrMod d) : v.val (Sum.inl 0) ^ 2 =
     (⟪v, v⟫ₘ) + ∑ i, v.val (Sum.inr i) ^ 2:= by
   rw [as_sum]
   apply sub_eq_iff_eq_add.mp
@@ -354,18 +356,18 @@ lemma inl_sq_eq (v : Contr d) : v.val (Sum.inl 0) ^ 2 =
   · funext i
     exact pow_two (v.val (Sum.inr i))
 
-lemma le_inl_sq (v : Contr d) : ⟪v, v⟫ₘ ≤ v.val (Sum.inl 0) ^ 2 := by
+lemma le_inl_sq (v : ContrMod d) : ⟪v, v⟫ₘ ≤ v.val (Sum.inl 0) ^ 2 := by
   rw [inl_sq_eq]
   apply (le_add_iff_nonneg_right _).mpr
   refine Fintype.sum_nonneg ?hf
   exact fun i => pow_two_nonneg (v.val (Sum.inr i))
 
-lemma ge_abs_inner_product (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
+lemma ge_abs_inner_product (v w : ContrMod d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
     ‖⟪v.toSpace, w.toSpace⟫_ℝ‖ ≤ ⟪v, w⟫ₘ := by
   rw [as_sum_toSpace, sub_le_sub_iff_left]
   exact Real.le_norm_self ⟪v.toSpace, w.toSpace⟫_ℝ
 
-lemma ge_sub_norm (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
+lemma ge_sub_norm (v w : ContrMod d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
     ‖v.toSpace‖ * ‖w.toSpace‖ ≤ ⟪v, w⟫ₘ := by
   apply le_trans _ (ge_abs_inner_product v w)
   rw [sub_le_sub_iff_left]
@@ -378,7 +380,7 @@ lemma ge_sub_norm (v w : Contr d) : v.val (Sum.inl 0) * w.val (Sum.inl 0) -
 -/
 
 @[simp]
-lemma basis_left {v : Contr d} (μ : Fin 1 ⊕ Fin d) :
+lemma basis_left {v : ContrMod d} (μ : Fin 1 ⊕ Fin d) :
     ⟪ ContrMod.stdBasis μ, v⟫ₘ = η μ μ * v.toFin1dℝ μ := by
   rw [as_sum]
   rcases μ with μ | μ