The construction of an element of the Lorentz group from a boost and a rotation #
The main result of this module is the homeomorphism toBoostRotation
from the restricted Lorentz group to the product of Lorentz velocities and rotations.
The inverse of this homeomorphism writes elements of the restricted Lorentz group as a product of a generalized boost and a rotation.
The Lorentz velocity obtained from toVector Λ
where Λ
is an element
of the restricted Lorentz group.
Equations
Instances For
A map from the restricted Lorentz group to rotations.
Equations
Instances For
The homeomorphism from the restricted Lorentz group to the product of
Lorentz.Velocity d
and Matrix.specialOrthogonalGroup (Fin d) ℝ
. The
inverse of this map writes an element of the restricted Lorentz group
as a product of a boost and a rotation.
Equations
- One or more equations did not get rendered due to their size.