Theorem Representation.IntertwiningMap.coe_id

Modification history

2026-08-14 05:41
Mathlib/RepresentationTheory/Intertwining.lean
chore(Data/Finsupp): make `mapDomain_congr` congr (#39575) …
Added Representation.IntertwiningMap.coe_idView on Github →