diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index 56e9df2baf..c2e4b3095e 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
@@ -20,13 +20,12 @@ which are used to define `realLorentzTensor`.
 
 open Matrix
 open MatrixGroups
-open Complex
 open TensorProduct
 
 namespace realLorentzTensor
 
 set_option backward.isDefEq.respectTransparency false in
-/-- The colors associated with complex representations of SL(2, ℂ) of interest to physics. -/
+/-- The colors associated with real representations of O(1, 3) of interest to physics. -/
 inductive Color
   /-- The color associated with contravariant Lorentz vectors. -/
   | up : Color
@@ -34,7 +33,7 @@ inductive Color
   | down : Color
 deriving Fintype
 
-/-- Color for complex Lorentz tensors is decidable. -/
+/-- Color for real Lorentz tensors is decidable. -/
 instance : DecidableEq Color := fun x y =>
   match x, y with
   | Color.up, Color.up => isTrue rfl
@@ -64,7 +63,7 @@ TODO "Replace Lorentz.ContrMod and Lorentz.CoMod in the definition of realLorent
 
 noncomputable section
 open realLorentzTensor in
-/-- The tensor structure for complex Lorentz tensors. -/
+/-- The tensor structure for real Lorentz tensors. -/
 def realLorentzTensor (d : ℕ := 3) : TensorSpecies
     ℝ realLorentzTensor.Color (LorentzGroup d)
     (fun | Color.up => Lorentz.ContrMod d | Color.down => Lorentz.CoMod d)
diff --git a/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
index f006a6b3be..ee46eef9fc 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean
@@ -29,11 +29,11 @@ namespace realLorentzTensor
 
 -/
 
-/-- The metric `ηᵢᵢ` as a complex Lorentz tensor. -/
+/-- The metric `ηᵢᵢ` as a real Lorentz tensor. -/
 abbrev coMetric (d : ℕ := 3) : ℝT[d, .down, .down] :=
   (realLorentzTensor d).metricTensor .down
 
-/-- The metric `ηⁱⁱ` as a complex Lorentz tensor. -/
+/-- The metric `ηⁱⁱ` as a real Lorentz tensor. -/
 abbrev contrMetric (d : ℕ := 3) : ℝT[d, .up, .up] :=
   (realLorentzTensor d).metricTensor .up
 
@@ -43,10 +43,10 @@ abbrev contrMetric (d : ℕ := 3) : ℝT[d, .up, .up] :=
 
 -/
 
-/-- The metric `ηᵢᵢ` as a complex Lorentz tensors. -/
+/-- The metric `ηᵢᵢ` as a real Lorentz tensors. -/
 scoped[realLorentzTensor] notation "η'" => @coMetric
 
-/-- The metric `ηⁱⁱ` as a complex Lorentz tensors. -/
+/-- The metric `ηⁱⁱ` as a real Lorentz tensors. -/
 scoped[realLorentzTensor] notation "η" => @contrMetric
 
 /-!