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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,657 to 1,662 of 2,569 results.
Lorentz.Vector.timeLike_iff_time_lt_space
Mathematical statement
A vector is timelike if and only if its time component squared is less than the sum of its spatial components squared
Source project: Physlib
Person-level attribution pending.
Lorentz.Vector.timelike_spatial_lt_time_squared
Mathematical statement
For timelike vectors, the spatial norm squared is strictly less than the time component squared
Source project: Physlib
Person-level attribution pending.
Lorentz.Vector.timelike_time_dominates_space
Mathematical statement
For timeLike vectors in Minkowski space, the inner product of the spatial part is less than the square of the time component
Source project: Physlib
Person-level attribution pending.
lorentzAlgebra.exp_isOrthochronous
Mathematical statement
The exponential of an element of the Lorentz algebra is orthochronous.
Source project: Physlib
Person-level attribution pending.
lorentzAlgebra.exp_mem_lorentzGroup
Mathematical 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
Mathematical statement
Two Lorentz transformations which are in the same connected component have the same determinant.
Source project: Physlib
Person-level attribution pending.