PhysLean Documentation

PhysLean.Relativity.LorentzGroup.Rotations

Rotations #

In this module we define rotations of in the Lorentz group.

The subgroup of rotations of the Lorentz group.

Equations
Instances For
    theorem LorentzGroup.mem_rotations_iff {d : } (Λ : (LorentzGroup d)) :
    Λ Rotations d Λ (Sum.inl 0) (Sum.inl 0) = 1 IsProper Λ

    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