is_lorentz_matrix_mul

theoremverified

If A and B are 4x4 Lorentz matrices, then their matrix product A * B is also a Lorentz matrix.

Statement

theorem is_lorentz_matrix_mul {A B : Matrix (Fin 4) (Fin 4) ℝ} (hA : is_lorentz_matrix A) (hB : is_lorentz_matrix B) : is_lorentz_matrix (A * B)

Source

Wald, General Relativity, ch. 1

Verified

11 Sep 2026

Axioms

Classical.choiceQuot.soundpropext

Built on 2

is_lorentz_matrixA 4x4 real matrix Λ is a Lorentz matrix if it preserves the Minkowski metric matrix, satisfying Λᵀ * minkowski_matrix * Λ =…
minkowski_matrixThe Minkowski metric matrix on ℝ⁴ with mostly-plus signature (-, +, +, +) is the 4x4 diagonal matrix with diagonal entries -1, 1, 1, 1.

Read back from the Lean

For all 4 × 4 real matrices A and B, if A is a Lorentz matrix and B is a Lorentz matrix, then their matrix product A * B is also a 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 product of two Lorentz matrices is a Lorentz matrix. -/
theorem is_lorentz_matrix_mul {A B : Matrix (Fin 4) (Fin 4) ℝ} (hA : is_lorentz_matrix A) (hB : is_lorentz_matrix B) : is_lorentz_matrix (A * B) := by
  dsimp [is_lorentz_matrix] at *
  rw [Matrix.transpose_mul]
  calc
    (B.transpose * A.transpose) * minkowski_matrix * (A * B)
      = B.transpose * (A.transpose * minkowski_matrix * A) * B := by simp only [Matrix.mul_assoc]
    _ = B.transpose * minkowski_matrix * B := by rw [hA]
    _ = minkowski_matrix := hB

Discuss this result Challenge it