Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 591 research declarations. Search 10,000 more complete Mathlib declarations.
591 results
Clear filterslorentzAlgebra.exp_isOrthochronous
Plain-language statement
The exponential of an element of the Lorentz algebra is orthochronous.
Source project: Physlib
Person-level attribution pending.
lorentzAlgebra.exp_mem_lorentzGroup
Plain-language statement
The exponential of an element of the Lorentz algebra is a member of the Lorentz group.
Source project: Physlib
Person-level attribution pending.
LorentzGroup.det_on_connected_component
Plain-language statement
Two Lorentz transformations which are in the same connected component have the same determinant.
Source project: Physlib
Person-level attribution pending.
LorentzGroup.generalizedBoost_timeComponent_eq
Plain-language statement
The time component of a generalised boost. A proof of this result can be found at the below link: https://leanprover.zulipchat.com/#narrow/channel/479953-Physlib/topic/Lorentz.20group/near/523249684
Source project: Physlib
Person-level attribution pending.
LorentzGroup.isOrthochronous_on_connected_component
Plain-language statement
Two Lorentz transformations which are in the same connected component are either both orthochronous or both not orthochronous.
Source project: Physlib
Person-level attribution pending.
LorentzGroup.mem_iff_transpose_mul_minkowskiMatrix_mul_self
Plain-language statement
A matrix Λ is in the Lorentz group if and only if it satisfies Λᵀ * η * Λ = η.
Source project: Physlib
Person-level attribution pending.