`BookProof.ChapterWignerLittleGroup.act_mul` (A B X : Matrix (Fin 2) (Fin 2) ℂ) : act (A * B) X = act A (act B X)

Initializing...

`BookProof.ChapterWignerLittleGroup.act_mul` (A B X : Matrix (Fin 2) (Fin 2) ℂ) : act (A * B) X = act A (act B X) · Prove2Me