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 filtersLorentz.preContrCoUnitVal_expand_tmul
Plain-language statement
Expansion of preContrCoUnitVal into basis.
Source project: Physlib
Person-level attribution pending.
Lorentz.SL2C.toLorentzGroup_det_one
Plain-language statement
The determinant of the image of SL(2, ℂ) in the Lorentz group is one.
Source project: Physlib
Person-level attribution pending.
Lorentz.SL2C.toLorentzGroup_fst_col
Plain-language statement
The first column of the Lorentz matrix formed from an element of SL(2, ℂ).
Source project: Physlib
Person-level attribution pending.
Lorentz.Vector.timeLike_iff_time_lt_space
Plain-language 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
Plain-language 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
Plain-language 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.