`BookProof.LorentzOrthochronous.lorentz_time_col` {l : Matrix (Fin 4) (Fin 4) ℝ} (h : IsLorentz l) : (l 0 0) ^ 2 = 1 + (l 1 0) ^ 2 + (l 2 0) ^ 2 + (l 3 0) ^ 2

Initializing...

`BookProof.LorentzOrthochronous.lorentz_time_col` {l : Matrix (Fin 4) (Fin 4) ℝ} (h : IsLorentz l) : (l 0 0) ^ 2 = 1 + (l 1 0) ^ 2 + (l 2 0) ^ 2 + (l 3 0) ^ 2 · Prove2Me