To Lorentz Group fst col
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.
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 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersLorentz.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.
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.
maximal_bound_antichain
Plain-language statement
At every point , the magnitude of the Carleson sum over an antichain of tiles is bounded by a constant depending on times a maximal function of . The maximal function uses, for each tile , a ball centered at the tile center with radius .
Source project: Carleson formalization
Person-level attribution pending.
MeasureTheory.dLpNorm_conjneg
Plain-language statement
The discrete normalized norm is unchanged by conjugating a function and reflecting its argument: .
Source project: Arithmetic Progressions Almost Periodicity
Person-level attribution pending.
MeasureTheory.dLpNorm_translate
Plain-language statement
Translation preserves the discrete normalized norm: for every group element , .
Source project: Arithmetic Progressions Almost Periodicity
Person-level attribution pending.