From b0f1ae79dbe3df721ea869047762f448bf1c9292 Mon Sep 17 00:00:00 2001
From: jstoobysmith <72603918+jstoobysmith@users.noreply.github.com>
Date: Fri, 19 Jul 2024 16:19:58 -0400
Subject: [PATCH] refactor: add newline

---
 HepLean/SpaceTime/LorentzTensor/Real/Basic.lean | 1 +
 1 file changed, 1 insertion(+)

diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
index 36d49e7..23f52e7 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Basic.lean
@@ -281,6 +281,7 @@ lemma mapIso_refl : mapIso d (Equiv.refl X) = Equiv.refl _ := rfl
 ## Sums
 
 -/
+
 /-- An equivalence that splits elements of `IndexValue d (Sum.elim TX TY)` into two components. -/
 def indexValueSumEquiv {X Y : Type} {TX : X → Colors} {TY : Y → Colors} :
     IndexValue d (Sum.elim TX TY) ≃ IndexValue d TX × IndexValue d TY where