Commit 2023-12-05 09:47 ac94cca1

View on Github →

chore: split RepresentationTheory.Action in multiple files (#8660) Splits Mathlib.RepresentationTheory.Action in multiple files.

Estimated changes

deleted def Action.Hom.comp
deleted def Action.Hom.id
deleted structure Action.Hom
deleted theorem Action.Iso.conj_ρ
deleted def Action.abelianAux
deleted theorem Action.add_hom
deleted theorem Action.associator_hom_hom
deleted theorem Action.associator_inv_hom
deleted theorem Action.comp_hom
deleted def Action.diagonal
deleted def Action.forget
deleted theorem Action.hom_ext
deleted theorem Action.id_hom
deleted theorem Action.leftDual_v
deleted theorem Action.leftDual_ρ
deleted def Action.leftRegular
deleted theorem Action.leftUnitor_hom_hom
deleted theorem Action.leftUnitor_inv_hom
deleted def Action.mkIso
deleted theorem Action.neg_hom
deleted def Action.ofMulAction
deleted theorem Action.ofMulAction_apply
deleted def Action.res
deleted def Action.resComp
deleted def Action.resId
deleted theorem Action.rightDual_v
deleted theorem Action.rightDual_ρ
deleted theorem Action.smul_hom
deleted theorem Action.sum_hom
deleted theorem Action.tensorUnit_rho
deleted theorem Action.tensorUnit_v
deleted theorem Action.tensor_hom
deleted theorem Action.tensor_rho
deleted theorem Action.tensor_v
deleted def Action.trivial
deleted theorem Action.whiskerLeft_hom
deleted theorem Action.whiskerRight_hom
deleted theorem Action.zero_hom
deleted def Action.ρAut
deleted theorem Action.ρ_one
deleted structure Action
added def Action.Hom.comp
added def Action.Hom.id
added structure Action.Hom
added theorem Action.Iso.conj_ρ
added theorem Action.comp_hom
added def Action.diagonal
added def Action.forget
added theorem Action.hom_ext
added theorem Action.id_hom
added def Action.mkIso
added def Action.res
added def Action.resComp
added def Action.resId
added def Action.trivial
added def Action.ρAut
added theorem Action.ρ_one
added structure Action
added theorem Action.add_hom
added theorem Action.neg_hom
added theorem Action.smul_hom
added theorem Action.sum_hom
added theorem Action.zero_hom
added theorem Action.leftDual_v
added theorem Action.leftDual_ρ
added theorem Action.rightDual_v
added theorem Action.rightDual_ρ
added theorem Action.tensorUnit_rho
added theorem Action.tensorUnit_v
added theorem Action.tensor_hom
added theorem Action.tensor_rho
added theorem Action.tensor_v
added theorem Action.whiskerLeft_hom