Provedcommons

The Minkowski metric is its own inverse

\htmlData{mx=2}{\htmlData{mx=0}{\operatorname{minkowskiMatrix}} \cdot \htmlData{mx=1}{\operatorname{minkowskiMatrix}}} \mathrel{\htmlData{mx=3}{=}} 1

What the notation means · or point at any symbol

minkowskiMatrix: Commons.minkowskiMatrix: a definition from the library, not special notation. Its name is its meaning; open it in Lean to see how it is defined. (Commons.minkowskiMatrix)
·Multiplication: minkowskiMatrix times minkowskiMatrix. (Commons.minkowskiMatrix * Commons.minko…)
=Equality: minkowskiMatrix · minkowskiMatrix and 1 are the same. (Commons.minkowskiMatrix * Commons.minko…)

theorem minkowski-metric-squares-to-one :
    Commons.minkowskiMatrix * Commons.minkowskiMatrix = 1

From our commons: Commons.minkowskiMatrix_mul_self in the Commons.Physics.Minkowski 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