Theorem Representation.IntertwiningMap.coe_eq_toLinearMap

Modification history

2026-09-08 10:36

Mathlib/RepresentationTheory/Intertwining.lean

chore: rename SemilinearMapClass.semilinearMap to LinearMap.ofClass (#43376) …

Deleted Representation.IntertwiningMap.coe_eq_toLinearMap View on Github →

2026-03-26 21:44

Mathlib/RepresentationTheory/Intertwining.lean

feat(RepresentationTheory/Intertwining): add one simp lemma to get rid of the auto coercion (#37234)

Added Representation.IntertwiningMap.coe_eq_toLinearMap View on Github →