Theorem Representation.IntertwiningMap.sub_toLinearMap

Modification history

2026-03-09 12:13
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentationTheory/Intertwining): Revert #35100 (#36394)
Added Representation.IntertwiningMap.sub_toLinearMapView on Github →
2026-03-07 22:58
Mathlib/RepresentationTheory/Intertwining.lean
feat: definition of a character of a representation (#35100) …
Deleted Representation.IntertwiningMap.sub_toLinearMapView on Github →
2026-03-03 14:05
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentationTheory/Intertwining): Generalise and add lemmas (#36047)
Added Representation.IntertwiningMap.sub_toLinearMapView on Github →