Theorem Representation.IntertwiningMap.id_apply

Modification history

2026-08-14 05:41
Mathlib/RepresentationTheory/Intertwining.lean
chore(Data/Finsupp): make `mapDomain_congr` congr (#39575) …
Modified Representation.IntertwiningMap.id_applyView on Github →
2026-03-06 22:04
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentatioTheory/IntertwiningMap): Add APIs for Equiv and TensorProduct (#36273)
Added Representation.IntertwiningMap.id_applyView on Github →
2026-01-30 17:31
Mathlib/RepresentationTheory/Intertwining.lean
feat: Schur's lemma for monoid representations (#33802) …
Deleted Representation.IntertwiningMap.id_applyView on Github →
2026-01-22 17:00
Mathlib/RepresentationTheory/Intertwining.lean
feat: definition of an intertwining map (#33221) …
Added Representation.IntertwiningMap.id_applyView on Github →