Rotations #
In this module we define rotations of in the Lorentz group.
The subgroup of rotations of the Lorentz group.
Equations
- LorentzGroup.Rotations d = { carrier := fun (Λ : ↑(LorentzGroup d)) => ↑Λ (Sum.inl 0) (Sum.inl 0) = 1 ∧ LorentzGroup.IsProper Λ, mul_mem' := ⋯, one_mem' := ⋯, inv_mem' := ⋯ }
Instances For
@[simp]
The group homomorphism from the special orthogonal group to the Lorentz group.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]