Def Representation.IntertwiningMap.equivLinearMapAsModule

Modification history

2026-01-22 17:00

Mathlib/RepresentationTheory/Intertwining.lean

feat: definition of an intertwining map (#33221) …

Added Representation.IntertwiningMap.equivLinearMapAsModule View on Github →