is_lorentz_matrix
def
A 4x4 real matrix Λ is a Lorentz matrix if it preserves the Minkowski metric matrix, satisfying Λᵀ * minkowski_matrix * Λ = minkowski_matrix.
Statement
def is_lorentz_matrix (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Prop
- Source
- Wald, General Relativity, ch. 1; Naber, The Geometry of Minkowski Spacetime, ch. 2
- Verified
- 11 Sep 2026
- Axioms
- none listed
- Built on 1
- minkowski_matrixThe Minkowski metric matrix on ℝ⁴ with mostly-plus signature (-, +, +, +) is the 4x4 diagonal matrix with diagonal entries -1, 1, 1, 1.
- Used by 2
- is_lorentz_matrix_mulIf A and B are 4x4 Lorentz matrices, then their matrix product A * B is also a Lorentz matrix.
- is_lorentz_matrix_oneThe 4x4 identity matrix is a Lorentz matrix.
Read back from the Lean
A 4x4 real matrix Λ satisfies is_lorentz_matrix if and only if the matrix product of the transpose of Λ, minkowski_matrix, and Λ is equal to minkowski_matrix.
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
/-- Predicate stating that a 4x4 real matrix is a Lorentz transformation matrix. -/ def is_lorentz_matrix (Λ : Matrix (Fin 4) (Fin 4) ℝ) : Prop := Λ.transpose * minkowski_matrix * Λ = minkowski_matrix