Theorem Representation.IntertwiningMap.add_toLinearMap

Modification history

2026-03-03 14:05

Mathlib/RepresentationTheory/Intertwining.lean

chore(RepresentationTheory/Intertwining): Generalise and add lemmas (#36047)

Added Representation.IntertwiningMap.add_toLinearMap View on Github →