Commit 2026-03-03 14:05 89bf6044

View on Github →

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

Estimated changes

Modified Mathlib/RepresentationTheory/Intertwining.lean

added theorem Representation.IntertwiningMap.add_comp

added theorem Representation.IntertwiningMap.add_toLinearMap

added theorem Representation.IntertwiningMap.coe_neg

modified theorem Representation.IntertwiningMap.coe_nsmul

added theorem Representation.IntertwiningMap.coe_sub

added theorem Representation.IntertwiningMap.coe_zsmul

modified def Representation.IntertwiningMap.comp

added theorem Representation.IntertwiningMap.comp_add

added theorem Representation.IntertwiningMap.comp_apply

added theorem Representation.IntertwiningMap.comp_def

added theorem Representation.IntertwiningMap.comp_smul

added theorem Representation.IntertwiningMap.comp_toLinearMap

added theorem Representation.IntertwiningMap.ext

added theorem Representation.IntertwiningMap.isIntertwining_assoc

added theorem Representation.IntertwiningMap.smul_comp

added theorem Representation.IntertwiningMap.smul_toLinearMap

added theorem Representation.IntertwiningMap.sub_toLinearMap

modified theorem Representation.IntertwiningMap.toLinearMap_injective

added theorem Representation.IntertwiningMap.zero_toLinearMap

modified structure Representation.IntertwiningMap