Theorem Representation.IntertwiningMap.add_comp

Modification history

2026-09-29 15:37
Mathlib/RepresentationTheory/Intertwining.lean
feat(RepresentationTheory): add two simp lemmas (#43649) …
Modified Representation.IntertwiningMap.add_compView on Github →
2026-03-03 14:05
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentationTheory/Intertwining): Generalise and add lemmas (#36047)
Added Representation.IntertwiningMap.add_compView on Github →