`BookProof.ChapterWignerLittleGroup.act_one` (X : Matrix (Fin 2) (Fin 2) ℂ) : act 1 X = X

Initializing...

`BookProof.ChapterWignerLittleGroup.act_one` (X : Matrix (Fin 2) (Fin 2) ℂ) : act 1 X = X · Prove2Me