Theorem Representation.IntertwiningMap.lTensor_comp_rTensor

Modification history

2026-04-06 15:21

Mathlib/RepresentationTheory/Intertwining.lean

chore(RepresentationTheory/Intertwining): slightly generalise two lemmas (#37694)

Modified Representation.IntertwiningMap.lTensor_comp_rTensor View on Github →

2026-03-06 22:04

Mathlib/RepresentationTheory/Intertwining.lean

chore(RepresentatioTheory/IntertwiningMap): Add APIs for Equiv and TensorProduct (#36273)

Added Representation.IntertwiningMap.lTensor_comp_rTensor View on Github →