`BookProof.ChapterMackeyImprimitivity.mackeyMap_norm` (ψ : E) (x : X) : ‖mackeyMap S s ψ x‖ = ‖S.p x ψ‖

Initializing...

`BookProof.ChapterMackeyImprimitivity.mackeyMap_norm` (ψ : E) (x : X) : ‖mackeyMap S s ψ x‖ = ‖S.p x ψ‖ · Prove2Me