From ab56f32c68a9f87d45cdab3100db992ba5b2ab53 Mon Sep 17 00:00:00 2001
From: Evan Reinhardt <190321808+ereinhardt8@users.noreply.github.com>
Date: Thu, 1 Oct 2026 20:51:40 -0400
Subject: [PATCH 1/2] doc(Relativity): Correct documentation for
 realLorentzTensor

---
 Physlib/Relativity/Tensors/RealTensor/Basic.lean         | 7 +++----
 Physlib/Relativity/Tensors/RealTensor/Metrics/Basic.lean | 8 ++++----
 2 files changed, 7 insertions(+), 8 deletions(-)

diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index 56e9df2baf..f8f4850da7 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 SO⁺(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
 
 /-!

From b14830e1e2048fc87e0d30b35d1db80b05c2cf2e Mon Sep 17 00:00:00 2001
From: ereinhardt8 <190321808+ereinhardt8@users.noreply.github.com>
Date: Fri, 2 Oct 2026 07:25:11 -0400
Subject: [PATCH 2/2] doc: Update group in
 Physlib/Relativity/Tensors/RealTensor/Basic.lean

Co-authored-by: Joseph Tooby-Smith <72603918+jstoobysmith@users.noreply.github.com>
---
 Physlib/Relativity/Tensors/RealTensor/Basic.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/Physlib/Relativity/Tensors/RealTensor/Basic.lean b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
index f8f4850da7..c2e4b3095e 100644
--- a/Physlib/Relativity/Tensors/RealTensor/Basic.lean
+++ b/Physlib/Relativity/Tensors/RealTensor/Basic.lean
@@ -25,7 +25,7 @@ open TensorProduct
 namespace realLorentzTensor
 
 set_option backward.isDefEq.respectTransparency false in
-/-- The colors associated with real representations of SO⁺(1, 3) 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