`BookProof.ChapterMackeyImprimitivity.ImprimitivitySystem.U_apply_inv` (g : G) (ψ : E) : S.U g (S.U g⁻¹ ψ) = ψ

Initializing...

`BookProof.ChapterMackeyImprimitivity.ImprimitivitySystem.U_apply_inv` (g : G) (ψ : E) : S.U g (S.U g⁻¹ ψ) = ψ · Prove2Me