diff --git a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
index eb28427..b72b913 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/Constructors.lean
@@ -270,13 +270,8 @@ open Matrix
 
 /-- The action of the Lorentz group on `ofReal v` is trivial. -/
 @[simp]
-lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r := by
-  refine ext' rfl ?_
-  funext i
-  erw [lorentzAction_smul_coord]
-  simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
-    Finset.sum_singleton, IndexValue]
-  rfl
+lemma lorentzAction_ofReal (r : ℝ) : Λ • ofReal d r = ofReal d r :=
+  lorentzAction_on_isEmpty Λ (ofReal d r)
 
 /-- The action of the Lorentz group on `ofVecUp v` is by vector multiplication. -/
 @[simp]
diff --git a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
index 515f1c9..14858ad 100644
--- a/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
+++ b/HepLean/SpaceTime/LorentzTensor/Real/LorentzAction.lean
@@ -139,4 +139,17 @@ instance lorentzAction : MulAction (LorentzGroup d) (RealLorentzTensor d X) wher
 @[simps!]
 instance : MulAction (LorentzGroup d) (Marked d X n) := lorentzAction
 
+/-- The action on an empty Lorentz tensor is trivial. -/
+lemma lorentzAction_on_isEmpty [IsEmpty X] (Λ : LorentzGroup d) (T : RealLorentzTensor d X) :
+    Λ • T = T := by
+  refine ext' rfl ?_
+  funext i
+  erw [lorentzAction_smul_coord]
+  simp only [Finset.univ_unique, Finset.univ_eq_empty, Finset.prod_empty, one_mul,
+    Finset.sum_singleton]
+  simp only [IndexValue, Unique.eq_default]
+
+/-! TODO: Show that the Lorentz action commutes with multiplication. -/
+/-! TODO: Show that the Lorentz action commutes with contraction. -/
+/-! TODO: Show that the Lorentz action commutes with rising and lowering indices. -/
 end RealLorentzTensor