Theorem Representation.Equiv.toLinearEquiv_apply

Modification history

2026-03-06 22:04
Mathlib/RepresentationTheory/Intertwining.lean
chore(RepresentatioTheory/IntertwiningMap): Add APIs for Equiv and TensorProduct (#36273)
Modified Representation.Equiv.toLinearEquiv_applyView on Github →
2026-02-24 17:56
Mathlib/RepresentationTheory/Intertwining.lean
feat: definition of equivalence of representations (#34888) …
Added Representation.Equiv.toLinearEquiv_applyView on Github →