Commit 2026-03-06 22:04 f3179c59

View on Github →

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

Estimated changes

Modified Mathlib/RepresentationTheory/Intertwining.lean

added theorem Representation.Equiv.apply_symm_apply

modified theorem Representation.Equiv.coe_invFun

added theorem Representation.Equiv.coe_symm

modified theorem Representation.Equiv.coe_toIntertwiningMap

modified theorem Representation.Equiv.coe_toLinearMap

modified theorem Representation.Equiv.conj_apply_self

added theorem Representation.Equiv.ext

added def Representation.Equiv.mk

added def Representation.Equiv.refl

added theorem Representation.Equiv.refl_apply

added def Representation.Equiv.symm

added theorem Representation.Equiv.symm_apply_apply

added theorem Representation.Equiv.symm_trans

added theorem Representation.Equiv.toIntertwiningMap_mk'

added theorem Representation.Equiv.toIntertwiningMap_refl

added theorem Representation.Equiv.toIntertwiningMap_trans

modified theorem Representation.Equiv.toLinearEquiv_apply

added theorem Representation.Equiv.toLinearEquiv_inj

added theorem Representation.Equiv.toLinearEquiv_injective

added theorem Representation.Equiv.toLinearEquiv_mk'

added theorem Representation.Equiv.toLinearMap_mk'

added theorem Representation.Equiv.toLinearMap_refl

added theorem Representation.Equiv.toLinearMap_symm

added theorem Representation.Equiv.toLinearMap_trans

added def Representation.Equiv.trans

added theorem Representation.Equiv.trans_apply

added theorem Representation.Equiv.trans_symm

modified structure Representation.Equiv

added theorem Representation.IntertwiningMap.id_apply

added def Representation.IntertwiningMap.lTensor

added theorem Representation.IntertwiningMap.lTensor_apply

added theorem Representation.IntertwiningMap.lTensor_comp_rTensor

added theorem Representation.IntertwiningMap.lTensor_id

added def Representation.IntertwiningMap.rTensor

added theorem Representation.IntertwiningMap.rTensor_apply

added theorem Representation.IntertwiningMap.rTensor_comp_lTensor

added theorem Representation.IntertwiningMap.rTensor_id

deleted theorem Representation.IntertwiningMap.smul_toLinearMap

added def Representation.IntertwiningMap.tensor

added theorem Representation.IntertwiningMap.tensor_apply

modified theorem Representation.IntertwiningMap.toLinearMap_apply

added theorem Representation.IntertwiningMap.toLinearMap_id

added theorem Representation.IntertwiningMap.toLinearMap_lTensor

added theorem Representation.IntertwiningMap.toLinearMap_mk

added theorem Representation.IntertwiningMap.toLinearMap_rTensor

added theorem Representation.IntertwiningMap.toLinearMap_smul

added theorem Representation.IntertwiningMap.toLinearMap_tensor

added def Representation.TensorProduct.assoc

added theorem Representation.TensorProduct.assoc_apply

added theorem Representation.TensorProduct.assoc_symm_toLinearMap

added def Representation.TensorProduct.comm

added theorem Representation.TensorProduct.comm_apply

added theorem Representation.TensorProduct.comm_comp_lTensor

added theorem Representation.TensorProduct.comm_comp_rTensor

added theorem Representation.TensorProduct.comm_symm

added def Representation.TensorProduct.lid

added theorem Representation.TensorProduct.lid_apply

added theorem Representation.TensorProduct.lid_symm_apply

added def Representation.TensorProduct.rid

added theorem Representation.TensorProduct.rid_apply

added theorem Representation.TensorProduct.rid_symm_apply

added theorem Representation.TensorProduct.toLinearMap_assoc

added theorem Representation.TensorProduct.toLinearMap_comm

added theorem Representation.TensorProduct.toLinearMap_lid

added theorem Representation.TensorProduct.toLinearMap_rid