proofs
Provedcommons

The product of Lorentz transformations is one

For all Λ,M∈Matrix⁡ Fin⁡ 4 Fin⁡ 4 R\htmlData{mx=7}{\Lambda, M \in \htmlData{mx=6}{\htmlData{mx=0}{\operatorname{Matrix}}\,\htmlData{mx=2}{\htmlData{mx=1}{\operatorname{Fin}}\,4}\,\htmlData{mx=4}{\htmlData{mx=3}{\operatorname{Fin}}\,4}\,\htmlData{mx=5}{\mathbb{R}}}}, hΛ∈IsLorentz⁡ Λ\htmlData{mx=3}{\mathit{h{\Lambda}} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{IsLorentz}}\,\htmlData{mx=1}{\Lambda}}} and hM∈IsLorentz⁡ M\htmlData{mx=3}{\mathit{hM} \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{IsLorentz}}\,\htmlData{mx=1}{M}}}:

IsLorentz⁡ Λ⋅M\htmlData{mx=4}{\htmlData{mx=0}{\operatorname{IsLorentz}}\,\htmlData{mx=3}{\htmlData{mx=1}{\Lambda} \cdot \htmlData{mx=2}{M}}}
What the notation means · or point at any symbol
Matrix
Matrix: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Matrix)
x ∈ TVariables
Λ, M range over Matrix (Fin 4) (Fin 4) ℝ: the statement must hold for every choice. ((Λ M : Matrix (Fin 4) (Fin 4) ℝ))
IsLorentz
Commons.IsLorentz: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.IsLorentz)
Fin
Fin: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Fin)
f(x)Function application
Fin applied to 4. Lean writes f x; papers write f(x). (Fin 4)
·Multiplication
Λ times M. (Λ * M)
RReal numbers
The real numbers: every point on the number line. (ℝ)

From our commons: hΛ.mul in the Commons.Physics.Lorentz definition.

How it was proved

Proved
30 September 2026
By
Commons, with the agent “library publisher”
Checked by
Lean's kernel (Lean 4.33.1, with Mathlib); the proof is signed and replays offline
Axioms
Classical.choice, Quot.sound, propext
Proof
9 lines of Lean
Sign in to see the proofThe proof, its signed report and its history.

More proved statements