`BookProof.ChapterMackeyImprimitivity.mackeyMap_add` (ψ φ : E) : mackeyMap S s (ψ + φ) = mackeyMap S s ψ + mackeyMap S s φ

Initializing...

`BookProof.ChapterMackeyImprimitivity.mackeyMap_add` (ψ φ : E) : mackeyMap S s (ψ + φ) = mackeyMap S s ψ + mackeyMap S s φ · Prove2Me