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,663 to 1,668 of 2,569 results.
LorentzGroup.generalizedBoost_timeComponent_eq
Mathematical 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
Mathematical 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
Mathematical statement
A matrix Λ is in the Lorentz group if and only if it satisfies Λᵀ * η * Λ = η.
Source project: Physlib
Person-level attribution pending.
map_construction
Mathematical statement
The T-transform is natural in any oracle-semantics morphism that preserves both the plaintext-to-coins query capability and the distinguished lift of ProbComp.
Source project: VCVio
Person-level attribution pending.
Matrix.blockTriangular_exp_of_blockTriangular_id
Mathematical statement
The exponential of an upper-triangular matrix is upper-triangular.
Source project: Physlib
Person-level attribution pending.
Matrix.det_exp
Mathematical statement
The determinant of the exponential of a matrix is the exponential of its trace. This is also known as Lie's trace formula.
Source project: Physlib
Person-level attribution pending.