`BookProof.LorentzOrthochronous.isPO_inv` {l : Matrix (Fin 4) (Fin 4) ℝ} (h : IsProperOrthochronous l) : IsProperOrthochronous l⁻¹

Initializing...

`BookProof.LorentzOrthochronous.isPO_inv` {l : Matrix (Fin 4) (Fin 4) ℝ} (h : IsProperOrthochronous l) : IsProperOrthochronous l⁻¹ · Prove2Me