is_lorentz_matrix_one
theoremverified
The 4x4 identity matrix is a Lorentz matrix.
Statement
theorem is_lorentz_matrix_one : is_lorentz_matrix 1- Source
- Wald, General Relativity, ch. 1
- Verified
- 11 Sep 2026
- Axioms
Classical.choiceQuot.soundpropext- Built on 1
- is_lorentz_matrixA 4x4 real matrix Λ is a Lorentz matrix if it preserves the Minkowski metric matrix, satisfying Λᵀ * minkowski_matrix * Λ =…
Read back from the Lean
The $4 \times 4$ identity matrix with real entries satisfies is_lorentz_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
/-- The 4x4 identity matrix is a Lorentz matrix. -/ theorem is_lorentz_matrix_one : is_lorentz_matrix 1 := by simp [is_lorentz_matrix]