`BookProof.ChapterA3.lambda_mem_lorentz` (S : Matrix (Fin 4) (Fin 4) ℝ) (hS : IsPin S) : LambdaOf S ∈ LorentzO

Initializing...

`BookProof.ChapterA3.lambda_mem_lorentz` (S : Matrix (Fin 4) (Fin 4) ℝ) (hS : IsPin S) : LambdaOf S ∈ LorentzO · Prove2Me