diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 0000000..794c3a1
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,12 @@
+# Contributing 
+
+## Adding results to HepLean
+
+This assumes you have already installed Lean and setup HepLean. 
+
+To add a result to HepLean:
+
+- Create a new branch of HepLean.
+- Name the branch something which tells people what sort of things you are adding e.g. "StandardModel-HiggsPotential"
+- On pushing to a brach GitHub will run a number of continous integration checks on your code.
+- Once you are happy, and your branch has passed the continous integration checks, make a pull-request to the main branch of HepLean.
diff --git a/HepLean/SpaceTime/LorentzGroup.lean b/HepLean/SpaceTime/LorentzGroup.lean
index 1fc8c66..1b858e9 100644
--- a/HepLean/SpaceTime/LorentzGroup.lean
+++ b/HepLean/SpaceTime/LorentzGroup.lean
@@ -4,16 +4,25 @@ Released under Apache 2.0 license.
 Authors: Joseph Tooby-Smith
 -/
 import HepLean.SpaceTime.Metric
+import Mathlib.GroupTheory.SpecificGroups.KleinFour
 /-!
 # The Lorentz Group
 
-We define the Lorentz group, and show it is a closed subgroup General Linear Group.
+We define the Lorentz group.
 
 ## TODO
 
 - Show that the Lorentz is a Lie group.
-- Define the proper Lorentz group.
-- Define the restricted Lorentz group, and prove it is connected.
+- Prove that the restricted Lorentz group is equivalent to the connected component of the
+identity.
+- Define the continuous maps from `ℝ³` to `restrictedLorentzGroup` defining boosts.
+
+## References
+
+- http://home.ku.edu.tr/~amostafazadeh/phys517_518/phys517_2016f/Handouts/A_Jaffi_Lorentz_Group.pdf
+- A proof that the restricted Lorentz group is connected can be found at:
+  https://diposit.ub.edu/dspace/bitstream/2445/68763/2/memoria.pdf
+  The proof involves the introduction of boosts.
 
 -/
 
@@ -72,9 +81,44 @@ lemma mem_lorentzGroup_iff'' (Λ : GL (Fin 4) ℝ) :
   · simp_all only [ηLin_apply_apply, implies_true, iff_true, one_mulVec]
   · simp_all only [ηLin_apply_apply, mulVec_mulVec, implies_true]
 
-lemma det_lorentzGroup (Λ : lorentzGroup) : Λ.1.1.det = 1 ∨ Λ.1.1.det = -1 := by
-  simpa [← sq, det_one, det_mul, det_mul, det_mul, det_transpose, det_η] using
-    (congrArg det ((mem_lorentzGroup_iff'' Λ.1).mp Λ.2))
+lemma mem_lorentzGroup_iff''' (Λ : GL (Fin 4) ℝ) :
+    Λ ∈ lorentzGroup ↔ η * Λ.1ᵀ * η = Λ⁻¹ := by
+  rw [mem_lorentzGroup_iff'']
+  exact Units.mul_eq_one_iff_eq_inv
+
+
+lemma mem_lorentzGroup_iff_transpose (Λ : GL (Fin 4) ℝ) :
+    Λ ∈ lorentzGroup ↔ ⟨transpose Λ, (transpose Λ)⁻¹, by
+        rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ).symm]
+        rw [show ((Λ)⁻¹).1 * Λ.1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.inv_mul_eq_one]]
+        rw [@transpose_eq_one], by
+        rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ).symm]
+        rw [show Λ.1 * ((Λ)⁻¹).1  = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.mul_inv_eq_one]]
+        rw [@transpose_eq_one]⟩  ∈ lorentzGroup := by
+  rw [mem_lorentzGroup_iff''', mem_lorentzGroup_iff''']
+  simp only [coe_units_inv, transpose_transpose, Units.inv_mk]
+  apply Iff.intro
+  intro h
+  have h1 := congrArg transpose h
+  rw [transpose_mul, transpose_mul, transpose_transpose, η_transpose, ← mul_assoc] at h1
+  rw [h1]
+  exact transpose_nonsing_inv _
+  intro h
+  have h1 := congrArg transpose h
+  rw [transpose_mul, transpose_mul, η_transpose, ← mul_assoc] at h1
+  rw [h1, transpose_nonsing_inv, transpose_transpose]
+
+/-- The transpose of an matrix in the Lorentz group is an element of the Lorentz group. -/
+def lorentzGroupTranspose (Λ : lorentzGroup) : lorentzGroup :=
+  ⟨⟨transpose Λ.1, (transpose Λ.1)⁻¹, by
+    rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ.1).symm]
+    rw [show ((Λ.1)⁻¹).1 * Λ.1 = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.inv_mul_eq_one]]
+    rw [@transpose_eq_one], by
+    rw [← transpose_nonsing_inv, ← transpose_mul, (coe_units_inv Λ.1).symm]
+    rw [show Λ.1.1 * ((Λ.1)⁻¹).1  = (1 : Matrix (Fin 4) (Fin 4) ℝ) by rw [@Units.mul_inv_eq_one]]
+    rw [@transpose_eq_one]⟩,
+    (mem_lorentzGroup_iff_transpose Λ.1).mp Λ.2 ⟩
+
 
 /-- A continous map from `GL (Fin 4) ℝ` to  `Matrix (Fin 4) (Fin 4) ℝ` for which the Lorentz
 group is the kernal. -/
@@ -90,10 +134,315 @@ lemma lorentzGroup_kernal : lorentzGroup = lorentzMap ⁻¹' {1} := by
   erw [mem_lorentzGroup_iff'' Λ]
   rfl
 
-theorem lorentzGroup_isClosed : IsClosed (lorentzGroup : Set (GeneralLinearGroup (Fin 4) ℝ)) := by
+/-- The Lorentz Group is a closed subset of `GL (Fin 4) ℝ`. -/
+theorem lorentzGroup_isClosed : IsClosed (lorentzGroup : Set (GL (Fin 4) ℝ)) := by
   rw [lorentzGroup_kernal]
   exact continuous_iff_isClosed.mp lorentzMap_continuous {1} isClosed_singleton
 
+namespace lorentzGroup
+
+
+lemma det_eq_one_or_neg_one (Λ : lorentzGroup) : Λ.1.1.det = 1 ∨ Λ.1.1.det = -1 := by
+  simpa [← sq, det_one, det_mul, det_mul, det_mul, det_transpose, det_η] using
+    (congrArg det ((mem_lorentzGroup_iff'' Λ.1).mp Λ.2))
+
+local notation  "ℤ₂" => Multiplicative (ZMod 2)
+
+/-- A group homomorphism from `lorentzGroup` to `ℤ₂` taking a matrix to
+0 if it's determinant is 1 and 1 if its determinant is -1.-/
+@[simps!]
+def detRep : lorentzGroup →* ℤ₂ where
+  toFun Λ := if Λ.1.1.det = 1 then (Additive.toMul 0) else Additive.toMul (1 : ZMod 2)
+  map_one' := by
+    simp
+  map_mul' := by
+    intro Λ1 Λ2
+    simp only [Submonoid.coe_mul, Subgroup.coe_toSubmonoid, Units.val_mul, det_mul, toMul_zero,
+      mul_ite, mul_one, ite_mul, one_mul]
+    cases' (det_eq_one_or_neg_one Λ1) with h1 h1
+      <;> cases' (det_eq_one_or_neg_one Λ2) with h2 h2
+      <;> simp [h1, h2]
+    rfl
+
+/-- A Lorentz Matrix is proper if its determinant is 1. -/
+def IsProper (Λ : lorentzGroup) : Prop := Λ.1.1.det = 1
+
+instance : DecidablePred IsProper := by
+  intro Λ
+  apply Real.decidableEq
+
+lemma IsProper_iff (Λ : lorentzGroup) :
+    IsProper Λ ↔ detRep Λ = Additive.toMul 0 := by
+  apply Iff.intro
+  intro h
+  erw [detRep_apply, if_pos h]
+  simp only [toMul_zero]
+  intro h
+  by_cases h1 : IsProper Λ
+  exact h1
+  erw [detRep_apply, if_neg h1] at h
+  contradiction
+
+section Orthochronous
+
+/-- The space-like part of the first row of of a Lorentz matrix. -/
+@[simp]
+def fstRowToEuclid (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 0 i.succ
+
+/-- The space-like part of the first column of of a Lorentz matrix. -/
+@[simp]
+def fstColToEuclid (Λ : lorentzGroup) : EuclideanSpace ℝ (Fin 3) := fun i => Λ.1 i.succ 0
+
+lemma fst_col_normalized (Λ : lorentzGroup) :
+    (Λ.1 0 0) ^ 2 - (Λ.1 1 0) ^ 2 - (Λ.1 2 0) ^ 2 - (Λ.1 3 0) ^ 2 = 1 := by
+  have h00 := congrFun (congrFun ((mem_lorentzGroup_iff'' Λ).mp Λ.2) 0) 0
+  simp only [Fin.isValue, mul_apply, transpose_apply, Fin.sum_univ_four, ne_eq, zero_ne_one,
+    not_false_eq_true, η_off_diagonal, zero_mul, add_zero, Fin.reduceEq, one_ne_zero, mul_zero,
+    zero_add, one_apply_eq] at h00
+  simp only [η, Fin.isValue, cons_val', cons_val_zero, empty_val', cons_val_fin_one, vecCons_const,
+    one_mul, mul_one, cons_val_one, head_cons, mul_neg, neg_mul, cons_val_two, Nat.succ_eq_add_one,
+    Nat.reduceAdd, tail_cons, cons_val_three, head_fin_const] at h00
+  rw [← h00]
+  ring
+
+lemma fst_row_normalized (Λ : lorentzGroup) :
+    (Λ.1 0 0) ^ 2 - (Λ.1 0 1) ^ 2 - (Λ.1 0 2) ^ 2 - (Λ.1 0 3) ^ 2 = 1 := by
+  simpa using fst_col_normalized (lorentzGroupTranspose Λ)
+
+
+lemma zero_zero_sq_col (Λ : lorentzGroup) :
+    (Λ.1 0 0) ^ 2 = 1 + (Λ.1 1 0) ^ 2 + (Λ.1 2 0) ^ 2 + (Λ.1 3 0) ^ 2 := by
+  rw [← fst_col_normalized Λ]
+  ring
+
+lemma zero_zero_sq_row (Λ : lorentzGroup) :
+    (Λ.1 0 0) ^ 2 = 1 + (Λ.1 0 1) ^ 2 + (Λ.1 0 2) ^ 2 + (Λ.1 0 3) ^ 2 := by
+  rw [← fst_row_normalized Λ]
+  ring
+
+lemma zero_zero_sq_col' (Λ : lorentzGroup) :
+    (Λ.1 0 0) ^ 2 = 1 + ‖fstColToEuclid Λ‖ ^ 2  := by
+  rw [zero_zero_sq_col, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
+  simp only [Fin.isValue, fstColToEuclid, Fin.succ_zero_eq_one, RCLike.inner_apply, conj_trivial,
+    Fin.succ_one_eq_two]
+  rw [show (Fin.succ 2) = 3 by rfl]
+  ring_nf
+
+lemma zero_zero_sq_row' (Λ : lorentzGroup) :
+    (Λ.1 0 0) ^ 2 = 1 + ‖fstRowToEuclid Λ‖ ^ 2  := by
+  rw [zero_zero_sq_row, ← @real_inner_self_eq_norm_sq, @PiLp.inner_apply, Fin.sum_univ_three]
+  simp only [Fin.isValue, fstRowToEuclid, Fin.succ_zero_eq_one, RCLike.inner_apply, conj_trivial,
+    Fin.succ_one_eq_two]
+  rw [show (Fin.succ 2) = 3 by rfl]
+  ring_nf
+
+lemma norm_col_leq_abs_zero_zero  (Λ : lorentzGroup) : ‖fstColToEuclid Λ‖ ≤ |Λ.1 0 0| := by
+  rw [(abs_norm (fstColToEuclid Λ)).symm, ← @sq_le_sq, zero_zero_sq_col']
+  simp only [le_add_iff_nonneg_left, zero_le_one]
+
+lemma norm_row_leq_abs_zero_zero (Λ : lorentzGroup)  : ‖fstRowToEuclid Λ‖ ≤ |Λ.1 0 0| := by
+  rw [(abs_norm (fstRowToEuclid Λ)).symm, ← @sq_le_sq, zero_zero_sq_row']
+  simp only [le_add_iff_nonneg_left, zero_le_one]
+
+
+
+lemma zero_zero_sq_ge_one (Λ : lorentzGroup) : 1 ≤ (Λ.1 0 0) ^ 2 := by
+  rw [zero_zero_sq_col Λ]
+  refine le_add_of_le_of_nonneg ?_ (sq_nonneg _)
+  refine le_add_of_le_of_nonneg ?_ (sq_nonneg _)
+  refine le_add_of_le_of_nonneg (le_refl 1) (sq_nonneg _)
+
+lemma abs_zero_zero_ge_one (Λ : lorentzGroup) : 1 ≤ |Λ.1 0 0| :=
+  (one_le_sq_iff_one_le_abs _).mp (zero_zero_sq_ge_one Λ)
+
+lemma zero_zero_le_minus_one_or_ge_one (Λ : lorentzGroup) : (Λ.1 0 0) ≤ - 1 ∨ 1 ≤ (Λ.1 0 0) :=
+  le_abs'.mp (abs_zero_zero_ge_one Λ)
+
+lemma zero_zero_nonpos_iff (Λ : lorentzGroup) : (Λ.1 0 0) ≤ 0 ↔ (Λ.1 0 0) ≤ - 1 := by
+  apply Iff.intro
+  · intro h
+    cases' zero_zero_le_minus_one_or_ge_one Λ with h1 h1
+    exact h1
+    linarith
+  · intro h
+    linarith
+
+lemma zero_zero_nonneg_iff (Λ : lorentzGroup) : 0 ≤ (Λ.1 0 0) ↔ 1 ≤ (Λ.1 0 0) := by
+  apply Iff.intro
+  · intro h
+    cases' zero_zero_le_minus_one_or_ge_one Λ with h1 h1
+    linarith
+    exact h1
+  · intro h
+    linarith
+
+/-- An element of the lorentz group is orthochronous if its time-time element is non-negative. -/
+@[simp]
+def IsOrthochronous (Λ : lorentzGroup) : Prop := 0 ≤ Λ.1 0 0
+
+instance : Decidable (IsOrthochronous Λ) :=
+  Real.decidableLE 0 (Λ.1 0 0)
+
+lemma not_IsOrthochronous_iff (Λ : lorentzGroup) : ¬ IsOrthochronous Λ ↔ Λ.1 0 0 ≤ 0 := by
+  rw [IsOrthochronous, not_le]
+  apply Iff.intro
+  intro h
+  exact le_of_lt h
+  intro h
+  have h1 := (zero_zero_nonpos_iff Λ).mp h
+  linarith
+
+
+lemma IsOrthochronous_abs_zero_zero {Λ : lorentzGroup} (h : IsOrthochronous Λ) :
+    |Λ.1 0 0| = Λ.1 0 0 :=
+  abs_eq_self.mpr h
+
+lemma not_IsOrthochronous_abs_zero_zero {Λ : lorentzGroup} (h : ¬ IsOrthochronous Λ) :
+    Λ.1 0 0  = - |Λ.1 0 0| := by
+  refine neg_eq_iff_eq_neg.mp (abs_eq_neg_self.mpr ?_).symm
+  simp only [IsOrthochronous, Fin.isValue, not_le] at h
+  exact le_of_lt h
+
+lemma schwartz_identity_fst_row_col (Λ Λ' : lorentzGroup) :
+    ‖⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ‖ ≤ ‖fstRowToEuclid Λ‖ * ‖fstColToEuclid Λ'‖ :=
+  norm_inner_le_norm (fstRowToEuclid Λ) (fstColToEuclid Λ')
+
+lemma zero_zero_mul (Λ Λ' : lorentzGroup) :
+    (Λ * Λ').1 0 0 = (Λ.1 0 0) * (Λ'.1 0 0) + ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ := by
+  rw [@Subgroup.coe_mul, @GeneralLinearGroup.coe_mul, mul_apply, Fin.sum_univ_four]
+  rw [@PiLp.inner_apply, Fin.sum_univ_three]
+  simp
+  rw [show (Fin.succ 2) = 3 by rfl]
+  ring_nf
+example (a b c : ℝ ) (h : a - b ≤ a + c) : - b ≤ c := by
+  exact (add_le_add_iff_left a).mp h
+
+lemma zero_zero_mul_sub_row_col (Λ Λ' : lorentzGroup) :
+    0 ≤ |Λ.1 0 0| * |Λ'.1 0 0| - ‖fstRowToEuclid Λ‖ * ‖fstColToEuclid Λ'‖ :=
+  sub_nonneg.mpr (mul_le_mul (norm_row_leq_abs_zero_zero Λ) (norm_col_leq_abs_zero_zero Λ')
+    (norm_nonneg (fstColToEuclid Λ')) (abs_nonneg (Λ.1 0 0)))
+
+lemma orthchro_mul_orthchro {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
+    (h' : IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
+  apply le_trans (zero_zero_mul_sub_row_col Λ Λ')
+  have h1 := zero_zero_mul Λ Λ'
+  rw [← IsOrthochronous_abs_zero_zero h, ← IsOrthochronous_abs_zero_zero h'] at h1
+  refine le_trans
+    (?_ : _ ≤ |Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|)) ?_
+  · erw [add_le_add_iff_left]
+    simp only [neg_mul, neg_neg, neg_le]
+    exact schwartz_identity_fst_row_col Λ Λ'
+  · rw [h1, add_le_add_iff_left]
+    exact neg_abs_le ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
+
+lemma not_orthchro_mul_not_orthchro {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ)
+    (h' : ¬ IsOrthochronous Λ') : IsOrthochronous (Λ * Λ') := by
+  apply le_trans (zero_zero_mul_sub_row_col Λ Λ')
+  refine le_trans
+    (?_ : _ ≤ |Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|)) ?_
+  · erw [add_le_add_iff_left]
+    simp only [neg_mul, neg_neg, neg_le]
+    exact schwartz_identity_fst_row_col Λ Λ'
+  · rw [zero_zero_mul Λ Λ', not_IsOrthochronous_abs_zero_zero h,
+      not_IsOrthochronous_abs_zero_zero h']
+    simp only [Fin.isValue, abs_neg, _root_.abs_abs, conj_trivial, mul_neg, neg_mul, neg_neg,
+      add_le_add_iff_left]
+    exact neg_abs_le ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
+
+lemma orthchro_mul_not_orthchro {Λ Λ' : lorentzGroup} (h : IsOrthochronous Λ)
+    (h' : ¬ IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
+  rw [not_IsOrthochronous_iff]
+  refine le_trans
+    (?_ : _ ≤ - (|Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|))) ?_
+  · rw [zero_zero_mul Λ Λ', ← IsOrthochronous_abs_zero_zero h,
+      not_IsOrthochronous_abs_zero_zero h']
+    simp only [Fin.isValue, mul_neg, _root_.abs_abs, abs_neg, neg_add_rev, neg_neg,
+      le_add_neg_iff_add_le, neg_add_cancel_comm]
+    exact le_abs_self ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
+  · apply le_trans ?_ (neg_nonpos_of_nonneg (zero_zero_mul_sub_row_col Λ Λ'))
+    simp only [Fin.isValue, neg_add_rev, neg_neg, neg_sub, add_neg_le_iff_le_add, sub_add_cancel]
+    exact schwartz_identity_fst_row_col _ _
+
+lemma not_orthchro_mul_orthchro {Λ Λ' : lorentzGroup} (h : ¬ IsOrthochronous Λ)
+    (h' : IsOrthochronous Λ') : ¬ IsOrthochronous (Λ * Λ') := by
+  rw [not_IsOrthochronous_iff]
+  refine le_trans
+    (?_ : _ ≤ - (|Λ.1 0 0| * |Λ'.1 0 0| + (- |⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ|))) ?_
+  · rw [zero_zero_mul Λ Λ', ← IsOrthochronous_abs_zero_zero h',
+      not_IsOrthochronous_abs_zero_zero h]
+    simp only [Fin.isValue, neg_mul, PiLp.inner_apply, fstRowToEuclid, fstColToEuclid,
+      RCLike.inner_apply, conj_trivial, abs_neg, _root_.abs_abs, neg_add_rev, neg_neg,
+      le_add_neg_iff_add_le, neg_add_cancel_comm]
+    exact le_abs_self ⟪fstRowToEuclid Λ, fstColToEuclid Λ'⟫_ℝ
+  · apply le_trans ?_ (neg_nonpos_of_nonneg (zero_zero_mul_sub_row_col Λ Λ'))
+    simp only [Fin.isValue, neg_add_rev, neg_neg, neg_sub, add_neg_le_iff_le_add, sub_add_cancel]
+    exact schwartz_identity_fst_row_col _ _
+
+/-- The homomorphism from `lorentzGroup` to `ℤ₂` whose kernal consists of precisely the
+orthochronous elements. -/
+@[simps!]
+def orthochronousRep : lorentzGroup →* ℤ₂ where
+  toFun Λ := if IsOrthochronous Λ then (Additive.toMul 0) else Additive.toMul (1 : ZMod 2)
+  map_one' := by
+    simp
+  map_mul' := by
+    intro Λ1 Λ2
+    simp only [toMul_zero, mul_ite, mul_one, ite_mul, one_mul]
+    cases' (em (IsOrthochronous Λ1)) with h h
+      <;> cases' (em (IsOrthochronous Λ2)) with h' h'
+    rw [if_pos (orthchro_mul_orthchro h h'), if_pos h, if_pos h']
+    rw [if_neg (orthchro_mul_not_orthchro h h'), if_neg h', if_pos h]
+    rw [if_neg (not_orthchro_mul_orthchro h h'), if_pos h', if_neg h]
+    rw [if_pos (not_orthchro_mul_not_orthchro h h'), if_neg h', if_neg h]
+    rfl
+
+lemma IsOrthochronous_iff (Λ : lorentzGroup) :
+    IsOrthochronous Λ ↔ orthochronousRep Λ = Additive.toMul 0 := by
+  apply Iff.intro
+  intro h
+  erw [orthochronousRep_apply, if_pos h]
+  simp only [toMul_zero]
+  intro h
+  by_cases h1 : IsOrthochronous Λ
+  exact h1
+  erw [orthochronousRep_apply, if_neg h1] at h
+  contradiction
+
+
+
+end Orthochronous
+
+end lorentzGroup
+
+open lorentzGroup in
+/-- The restricted lorentz group consists of those elements of the `lorentzGroup` which are
+proper and orthochronous. -/
+def restrictedLorentzGroup : Subgroup (lorentzGroup) where
+  carrier := {Λ | IsProper Λ ∧ IsOrthochronous Λ}
+  mul_mem' {Λa Λb} := by
+    intro ha hb
+    apply And.intro
+    rw [IsProper_iff, detRep.map_mul, (IsProper_iff Λa).mp ha.1, (IsProper_iff Λb).mp hb.1]
+    simp only [toMul_zero, mul_one]
+    rw [IsOrthochronous_iff, orthochronousRep.map_mul, (IsOrthochronous_iff Λa).mp ha.2,
+      (IsOrthochronous_iff Λb).mp hb.2]
+    simp
+  one_mem' := by
+    simp only [IsOrthochronous, Fin.isValue, Set.mem_setOf_eq, OneMemClass.coe_one, Units.val_one,
+      one_apply_eq, zero_le_one, and_true]
+    rw [IsProper_iff, detRep.map_one]
+    simp
+  inv_mem' {Λ} := by
+    intro h
+    apply And.intro
+    rw [IsProper_iff, detRep.map_inv, (IsProper_iff Λ).mp h.1]
+    simp only [toMul_zero, inv_one]
+    rw [IsOrthochronous_iff, orthochronousRep.map_inv, (IsOrthochronous_iff Λ).mp h.2]
+    simp
+
+/-- The restricted lorentz group is a topological group. -/
+instance : TopologicalGroup restrictedLorentzGroup :=
+  Subgroup.instTopologicalGroupSubtypeMem restrictedLorentzGroup
 
 end spaceTime
 
diff --git a/README.md b/README.md
index 651f908..648044d 100644
--- a/README.md
+++ b/README.md
@@ -39,11 +39,13 @@ If you want permission to create a pull-request for this repository contact Jose
 
 ### Installing Lean 4 
 
-See: https://leanprover-community.github.io/get_started.html
+The installation instructions for Lean 4 are given here: https://leanprover-community.github.io/get_started.html. 
 
-### Quick installation 
+### Installing HepLean 
 
-- clone this repository
-- Open a terminal in the corresponding directory.
-- Run `lake exe cache get`.
-- Rune `lake build`. 
+- Clone this repository (or download the repository as a Zip file) 
+- Open a terminal at the top-level in the corresponding directory.
+- Run `lake exe cache get`. The command `lake` should have been installed when you installed Lean.
+- Run `lake build`.
+- Open the directory (not a single file) in Visual Studio Code (or another Lean compatible code editor).
+