The Restricted Lorentz Group

This file is currently a stub.

def LorentzGroup.restricted (d : ℕ) : Subgroup ↑(LorentzGroup d)

The restricted Lorentz group comprises the proper and orthochronous elements of the Lorentz group.

Equations

• LorentzGroup.restricted d = { carrier := {Λ : ↑(LorentzGroup d) | LorentzGroup.IsProper Λ ∧ LorentzGroup.IsOrthochronous Λ}, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }

theorem LorentzGroup.restricted_normal_subgroup {d : ℕ} : (restricted d).Normal

The restricted Lorentz group is a normal subgroup of the Lorentz group.