Theorem Representation.IntertwiningMap.isIntertwiningMap_of_mem_center

Modification history

2026-01-22 17:00
Mathlib/RepresentationTheory/Intertwining.lean
feat: definition of an intertwining map (#33221) …
Added Representation.IntertwiningMap.isIntertwiningMap_of_mem_centerView on Github →