diff --git a/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean b/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean
index f42a69c9a..4cd482383 100644
--- a/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean
+++ b/Physlib/Relativity/LorentzGroup/Restricted/Basic.lean
@@ -16,9 +16,6 @@ This file is currently a stub.
 
 @[expose] public section
 
-TODO "Prove that every member of the restricted Lorentz group is
-  combination of a boost and a rotation."
-
 namespace LorentzGroup
 
 open Matrix
diff --git a/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean b/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean
index 83ca99d28..f9688ad8e 100644
--- a/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean
+++ b/Physlib/Relativity/LorentzGroup/Restricted/FromBoostRotation.lean
@@ -102,6 +102,14 @@ def toBoostRotation {d} : LorentzGroup.restricted d ≃ₜ Lorentz.Velocity d ×
   continuous_toFun := by fun_prop
   continuous_invFun := by fun_prop
 
+/-- Every element of the restricted Lorentz group can be written as a product of a
+  generalized boost and a rotation. -/
+theorem exists_boost_mul_rotation {d} (Λ : LorentzGroup.restricted d) :
+    ∃ (v : Lorentz.Velocity d) (R : Rotations d),
+      (Λ : LorentzGroup d) = generalizedBoost 0 v * (R : LorentzGroup d) := by
+  have h : toRotation Λ = (generalizedBoost 0 (toVelocity Λ))⁻¹ * Λ := rfl
+  exact ⟨toVelocity Λ, toRotation Λ, by rw [h, mul_inv_cancel_left]⟩
+
 end LorentzGroup
 
 end