`BookProof.ChapterA3.lorentz_of_conjR` (S : Matrix (Fin 4) (Fin 4) ℝ) (hS : IsUnit S.det) (Λ : Matrix (Fin 4) (Fin 4) ℝ) (hΛ : HasLambda S Λ) : Λ * minkowskiMat * Λᵀ = minkowskiMat

Initializing...

`BookProof.ChapterA3.lorentz_of_conjR` (S : Matrix (Fin 4) (Fin 4) ℝ) (hS : IsUnit S.det) (Λ : Matrix (Fin 4) (Fin 4) ℝ) (hΛ : HasLambda S Λ) : Λ * minkowskiMat * Λᵀ = minkowskiMat · Prove2Me