From da37263179e030e651cc3c56c38c1f6fea979232 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Tue, 11 Jun 2024 11:33:50 -0400
Subject: [PATCH] refactor: Lint

---
 HepLean.lean                                |  1 +
 HepLean/SpaceTime/LorentzAlgebra/Basis.lean | 10 +---------
 HepLean/SpaceTime/Metric.lean               | 14 ++++++++++----
 3 files changed, 12 insertions(+), 13 deletions(-)

diff --git a/HepLean.lean b/HepLean.lean
index 8972e40..2ca63bf 100644
--- a/HepLean.lean
+++ b/HepLean.lean
@@ -60,6 +60,7 @@ import HepLean.SpaceTime.Basic
 import HepLean.SpaceTime.CliffordAlgebra
 import HepLean.SpaceTime.FourVelocity
 import HepLean.SpaceTime.LorentzAlgebra.Basic
+import HepLean.SpaceTime.LorentzAlgebra.Basis
 import HepLean.SpaceTime.LorentzGroup.Basic
 import HepLean.SpaceTime.LorentzGroup.Boosts
 import HepLean.SpaceTime.LorentzGroup.Orthochronous
diff --git a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
index 25245fa..f7143d2 100644
--- a/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
+++ b/HepLean/SpaceTime/LorentzAlgebra/Basis.lean
@@ -11,24 +11,16 @@ We define the standard basis of the Lorentz group.
 
 -/
 
-
-
-
-
-
 namespace spaceTime
 
 namespace lorentzAlgebra
 open Matrix
 
-
-
+/-- The matrices which form the basis of the Lorentz algebra. -/
 @[simp]
 def σMat (μ ν : Fin 4) : Matrix (Fin 4) (Fin 4) ℝ := fun ρ δ ↦
   η^[ρ]_[μ] * η_[ν]_[δ] - η_[μ]_[δ] * η^[ρ]_[ν]
 
-
-
 end lorentzAlgebra
 
 end spaceTime
diff --git a/HepLean/SpaceTime/Metric.lean b/HepLean/SpaceTime/Metric.lean
index 5d428e0..67ce30b 100644
--- a/HepLean/SpaceTime/Metric.lean
+++ b/HepLean/SpaceTime/Metric.lean
@@ -29,18 +29,24 @@ open TensorProduct
 def η : Matrix (Fin 4) (Fin 4) ℝ := Matrix.reindex finSumFinEquiv finSumFinEquiv
   $ LieAlgebra.Orthogonal.indefiniteDiagonal (Fin 1) (Fin 3) ℝ
 
+/-- The metric with lower indices. -/
 notation "η_[" μ "]_[" ν "]" => η μ ν
 
+/-- The metric with upper indices. -/
 notation "η^[" μ "]^[" ν "]" => η μ ν
 
-notation "η_[" μ "]^[" ν "]" => η_[μ]_[0] * η^[0]^[ν] + η_[μ]_[1] * η^[1]^[ν] + η_[μ]_[2] * η^[2]^[ν]
-  + η_[μ]_[3] * η^[3]^[ν]
+/-- The metric with one lower and one upper index. -/
+notation "η_[" μ "]^[" ν "]" => η_[μ]_[0] * η^[0]^[ν] + η_[μ]_[1] * η^[1]^[ν] +
+  η_[μ]_[2] * η^[2]^[ν] + η_[μ]_[3] * η^[3]^[ν]
 
-notation "η^[" μ "]_[" ν "]" => η^[μ]^[0] * η_[0]_[ν] + η^[μ]^[1] * η_[1]_[ν] + η^[μ]^[2] * η_[2]_[ν]
-  + η^[μ]^[3] * η_[3]_[ν]
+/-- The metric with one lower and one upper index. -/
+notation "η^[" μ "]_[" ν "]" => η^[μ]^[0] * η_[0]_[ν] + η^[μ]^[1] * η_[1]_[ν]
+  + η^[μ]^[2] * η_[2]_[ν] + η^[μ]^[3] * η_[3]_[ν]
 
+/-- A matrix with one lower and one upper index. -/
 notation "["Λ"]^[" μ "]_[" ν "]" => (Λ : Matrix (Fin 4) (Fin 4) ℝ) μ ν
 
+/-- A matrix with both lower indices. -/
 notation "["Λ"]_[" μ "]_[" ν "]" => ∑ ρ, η_[μ]_[ρ] * [Λ]^[ρ]_[ν]