Commit 2024-10-24 19:49 1cc8fd22

View on Github →

chore(Algebra/Group/Action): reduce theory included with Group.Action.Defs (#18187) The Group/Action/Defs.lean file depends on a bit of theory and in turn defines some results not needed for e.g. modules. This PR tries to ensure that the focus is on the definitions of MulAction, SMulCommClass and IsScalarTower. In the process, I made the following moves:

  • Action/End.lean now contains the definition of Function.End and some results relating homomorphisms with multiplication
  • Action/Faithful.lean now contains the definition of FaithfulAction
  • Action/Pretransitive.lean now contains the definition of PretransitiveAction
  • Action/TypeTags.lean now contains the Additive/Multiplicative instances.

Estimated changes

deleted def AddAction.toEndHom
deleted theorem Function.End.mul_def
deleted theorem Function.End.one_def
deleted theorem Function.End.smul_def
deleted theorem MulAction.exists_smul_eq
deleted theorem MulAction.surjective_smul
deleted def MulAction.toEndHom
deleted theorem ofAdd_smul
deleted theorem ofMul_vadd
deleted theorem smul_left_injective'
deleted theorem toAdd_vadd
deleted theorem toMul_smul
added theorem Function.End.mul_def
added theorem Function.End.one_def
added theorem Function.End.smul_def
added theorem smul_left_injective'
added theorem ofAdd_smul
added theorem ofMul_vadd
added theorem toAdd_vadd
added theorem toMul_smul