Provedcommons

A Lorentz transformation has determinant ±1

For all $\htmlData{mx=7}{\Lambda \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}}}}$ and $\htmlData{mx=3}{h \in \htmlData{mx=2}{\htmlData{mx=0}{\operatorname{IsLorentz}}\,\htmlData{mx=1}{\Lambda}}}$ :

\htmlData{mx=3}{\htmlData{mx=2}{\operatorname{det}\left(\htmlData{mx=1}{\Lambda}\right)}^{2}} \mathrel{\htmlData{mx=4}{=}} 1

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)
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)
e.fdet: det of Λ: Lean's dot notation e.det means det applied to e. (Λ.det)
aᵇPower: Λ.det raised to the power 2. (Λ.det ^ 2)
=Equality: Λ.det^2 and 1 are the same. (Λ.det ^ 2 = 1)
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)
RReal numbers: The real numbers: every point on the number line. (ℝ)

theorem lorentz-determinant (Λ : Matrix (Fin 4) (Fin 4) ℝ) (h : Commons.IsLorentz Λ) :
    Λ.det ^ 2 = 1

From our commons: h.det_sq 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

A Lorentz transformation has determinant ±1

How it was proved

More proved statements