Commit 2026-03-09 12:13 4db86fbe

View on Github →

chore(RepresentationTheory/Intertwining): Revert #35100 (#36394)

Estimated changes

Modified Mathlib/RepresentationTheory/Intertwining.lean

modified theorem Representation.IntertwiningMap.coe_neg

modified theorem Representation.IntertwiningMap.coe_zsmul

added theorem Representation.IntertwiningMap.sub_toLinearMap

modified theorem Representation.IntertwiningMap.toLinearMap_apply