Commit 2026-09-29 11:07 4349c598

View on Github →

chore(RepresentationTheory/Equiv): generalize to Type* (#44073) This file has nothing to do with category theory so we can use Type* safely. α and W sharing the same universe w' aroud finsuppTensor is problematic. I found this from CI #41808 68fe33a

Estimated changes

Modified Mathlib/RepresentationTheory/Equiv.lean

modified def Representation.finsuppTensorLeft

modified theorem Representation.finsuppTensorLeft_apply_tmul

modified theorem Representation.finsuppTensorLeft_apply_tmul_apply

modified theorem Representation.finsuppTensorLeft_symm_apply_single

modified def Representation.finsuppTensorRight

modified theorem Representation.finsuppTensorRight_apply_tmul

modified theorem Representation.finsuppTensorRight_apply_tmul_apply

modified theorem Representation.finsuppTensorRight_symm_apply_single

modified def Representation.freeLift

modified def Representation.freeLiftLEquiv

modified theorem Representation.freeLift_single_single

modified def Representation.leftRegularTensorTrivialIsoFree

modified theorem Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single

modified theorem Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single