Commit 2024-10-25 05:50 fc157081

View on Github →

chore(Algebra/GroupWithZero/Action): reduce theory included with Group.Action.Defs (#18190) The GroupWithZero/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 SMulZeroClass and DistribMulAction. In the process, I made the following moves:

  • Action/End.lean now contains results involving Function.End and some results relating homomorphisms with multiplication
  • Action/Faithful.lean now contains results involving FaithfulAction

Estimated changes

deleted theorem AddMonoid.End.smul_def
deleted theorem Commute.smul_left_iff₀
deleted theorem Commute.smul_right_iff₀
deleted def Equiv.smulRight
deleted theorem eq_inv_smul_iff₀
deleted theorem inv_smul_eq_iff₀
deleted theorem inv_smul_smul₀
deleted theorem smul_inv_smul₀
added theorem AddMonoid.End.smul_def
added def Equiv.smulRight
added theorem eq_inv_smul_iff₀
added theorem inv_smul_eq_iff₀
added theorem inv_smul_smul₀
added theorem smul_inv_smul₀