minkowski_matrix
def
The Minkowski metric matrix on ℝ⁴ with mostly-plus signature (-, +, +, +) is the 4x4 diagonal matrix with diagonal entries -1, 1, 1, 1.
Statement
def minkowski_matrix : Matrix (Fin 4) (Fin 4) ℝ- Source
- Wald, General Relativity, ch. 1; Misner, Thorne & Wheeler, Gravitation, ch. 2
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Used by 2
- is_lorentz_matrixA 4x4 real matrix Λ is a Lorentz matrix if it preserves the Minkowski metric matrix, satisfying Λᵀ * minkowski_matrix * Λ =…
- is_lorentz_matrix_mulIf A and B are 4x4 Lorentz matrices, then their matrix product A * B is also a Lorentz matrix.
Read back from the Lean
minkowski_matrix is defined as the $4 \times 4$ real matrix Matrix.diagonal ![-1, 1, 1, 1], which is the diagonal matrix indexed by Fin 4 whose diagonal entries are $-1, 1, 1, 1$. That is, for $i, j \in \{0, 1, 2, 3\}$, the $(i, j)$-entry is $-1$ if $i = j = 0$, $1$ if $i = j \in \{1, 2, 3\}$, and $0$ if $i \neq j$.
Written by a model that saw only the Lean, never the English above. If the two disagree, that is worth a challenge.
Lean source view module on GitHub
/-- The standard Minkowski metric matrix with signature (-, +, +, +) on ℝ⁴. -/ def minkowski_matrix : Matrix (Fin 4) (Fin 4) ℝ := Matrix.diagonal ![-1, 1, 1, 1]