Commit 2026-03-09 18:39 3741129a

View on Github →

feat(RepresentationTheory/Action): Create representation from Action, second step of refactor Rep (#36341)

Estimated changes

Modified Mathlib.lean

Created Mathlib/RepresentationTheory/Action.lean

added theorem Action.tensor_ρ_apply

added theorem Representation.LinearizeMonoidal.assoc_comp_δ

added theorem Representation.LinearizeMonoidal.lTensor_comp_δ

added theorem Representation.LinearizeMonoidal.leftUnitor_δ

added def Representation.LinearizeMonoidal.linearizeDiagonalEquiv

added def Representation.LinearizeMonoidal.linearizeOfMulActionIso

added def Representation.LinearizeMonoidal.linearizeTrivialIso

added theorem Representation.LinearizeMonoidal.linearizeTrivialIso_apply

added theorem Representation.LinearizeMonoidal.linearizeTrivialIso_symm_apply

added theorem Representation.LinearizeMonoidal.linearizeTrivial_def

added theorem Representation.LinearizeMonoidal.rTensor_comp_δ

added theorem Representation.LinearizeMonoidal.rightUnitor_δ

added def Representation.LinearizeMonoidal.δ

added theorem Representation.LinearizeMonoidal.δ_apply_single

added theorem Representation.LinearizeMonoidal.δ_μ

added def Representation.LinearizeMonoidal.ε

added theorem Representation.LinearizeMonoidal.ε_one

added theorem Representation.LinearizeMonoidal.ε_η

added def Representation.LinearizeMonoidal.η

added theorem Representation.LinearizeMonoidal.η_single

added theorem Representation.LinearizeMonoidal.η_ε

added def Representation.LinearizeMonoidal.μ

added theorem Representation.LinearizeMonoidal.μ_apply_apply

added theorem Representation.LinearizeMonoidal.μ_apply_single_single

added theorem Representation.LinearizeMonoidal.μ_comp_assoc

added theorem Representation.LinearizeMonoidal.μ_comp_lTensor

added theorem Representation.LinearizeMonoidal.μ_comp_rTensor

added theorem Representation.LinearizeMonoidal.μ_leftUnitor

added theorem Representation.LinearizeMonoidal.μ_rightUnitor

added theorem Representation.LinearizeMonoidal.μ_δ

added def Representation.linearize

added def Representation.linearizeMap

added theorem Representation.linearizeMap_single

added theorem Representation.linearizeMap_toLinearMap

added theorem Representation.linearize_single

Created Mathlib/RepresentationTheory/Equiv.lean

added def Representation.diagonalOneEquivLeftRegular

added theorem Representation.diagonalOneEquivLeftRegular_apply_single

added theorem Representation.diagonalOneEquivLeftRegular_symm_apply_single

added def Representation.finsuppTensorLeft

added theorem Representation.finsuppTensorLeft_apply_tmul

added theorem Representation.finsuppTensorLeft_apply_tmul_apply

added theorem Representation.finsuppTensorLeft_symm_apply_single

added def Representation.finsuppTensorRight

added theorem Representation.finsuppTensorRight_apply_tmul

added theorem Representation.finsuppTensorRight_apply_tmul_apply

added theorem Representation.finsuppTensorRight_symm_apply_single

added def Representation.freeLift

added def Representation.freeLiftLEquiv

added theorem Representation.freeLift_single_single

added def Representation.leftRegularMapEquiv

added theorem Representation.leftRegularMapEquiv_symm_single

added def Representation.leftRegularTensorTrivialIsoFree

added theorem Representation.leftRegularTensorTrivialIsoFree_apply_single_tmul_single

added theorem Representation.leftRegularTensorTrivialIsoFree_symm_apply_single_single

added def Representation.ofMulActionSubsingletonEquivTrivial

added theorem Representation.ofMulActionSubsingletonEquivTrivial_apply

added theorem Representation.ofMulActionSubsingletonEquivTrivial_symm_apply

Modified Mathlib/RepresentationTheory/Intertwining.lean

added theorem LinearEquiv.isIntertwining_symm_isIntertwining

added theorem Representation.Equiv.mk_apply

added theorem Representation.Equiv.mk_symm