`BookProof.ChapterA3.massive_little_group` : {T : Matrix (Fin 2) (Fin 2) ℂ | T.det = 1 ∧ FixesTimeAxis (Upsilon T)} = SUtwo

Initializing...

`BookProof.ChapterA3.massive_little_group` : {T : Matrix (Fin 2) (Fin 2) ℂ | T.det = 1 ∧ FixesTimeAxis (Upsilon T)} = SUtwo · Prove2Me