Theorem Representation.IntertwiningMap.toLinearMap_apply

Modification history

2026-03-09 12:13
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentationTheory/Intertwining): Revert #35100 (#36394)
Modified Representation.IntertwiningMap.toLinearMap_applyView on Github →
2026-03-07 22:58
Mathlib/RepresentationTheory/Intertwining.lean
feat: definition of a character of a representation (#35100) …
Modified Representation.IntertwiningMap.toLinearMap_applyView on Github →
2026-03-06 22:04
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentatioTheory/IntertwiningMap): Add APIs for Equiv and TensorProduct (#36273)
Modified Representation.IntertwiningMap.toLinearMap_applyView on Github →
2026-01-30 06:41
Mathlib/RepresentationTheory/Intertwining.lean
style: fix whitespace (#34582) …
Modified Representation.IntertwiningMap.toLinearMap_applyView on Github →
2026-01-22 17:00
Mathlib/RepresentationTheory/Intertwining.lean
feat: definition of an intertwining map (#33221) …
Added Representation.IntertwiningMap.toLinearMap_applyView on Github →