Theorem Representation.IntertwiningMap.coe_nsmul

Modification history

2026-03-03 14:05
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentationTheory/Intertwining): Generalise and add lemmas (#36047)
Modified Representation.IntertwiningMap.coe_nsmulView on Github →
2026-01-22 17:00
Mathlib/RepresentationTheory/Intertwining.lean
feat: definition of an intertwining map (#33221) …
Added Representation.IntertwiningMap.coe_nsmulView on Github →