Commit 2025-02-26 11:41 1259f394

View on Github →

chore: move MulDistribMulAction under Algebra.Group (#20773) The motivation is that it is additivisable (even though it currently isn't) and is used in group theory files.

Estimated changes

Modified Mathlib/Algebra/BigOperators/GroupWithZero/Action.lean

Modified Mathlib/Algebra/Group/Action/Basic.lean

added def MulDistribMulAction.toMonoidEnd

added def MulDistribMulAction.toMonoidHom

added theorem smul_div'

added theorem smul_inv'

added theorem smul_pow'

Modified Mathlib/Algebra/Group/Action/Defs.lean

added theorem smul_mul'

Modified Mathlib/Algebra/Group/Action/End.lean

added def MulDistribMulAction.toMulEquiv

Modified Mathlib/Algebra/Group/Submonoid/Pointwise.lean

Modified Mathlib/Algebra/GroupWithZero/Action/Basic.lean

deleted def MulDistribMulAction.toMulEquiv

Modified Mathlib/Algebra/GroupWithZero/Action/Defs.lean

deleted def MulDistribMulAction.toMonoidHom

deleted theorem MulDistribMulAction.toMonoidHom_apply

deleted theorem smul_div'

deleted theorem smul_inv'

deleted theorem smul_mul'

deleted theorem smul_pow'

Modified Mathlib/Algebra/GroupWithZero/Action/End.lean

deleted def MulDistribMulAction.toMonoidEnd

Modified Mathlib/Algebra/GroupWithZero/Action/Opposite.lean

Modified Mathlib/Algebra/Module/Defs.lean

Modified Mathlib/Algebra/Ring/Action/Basic.lean

Modified Mathlib/GroupTheory/Congruence/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

Modified Mathlib/GroupTheory/GroupAction/DomAct/Basic.lean

Modified Mathlib/RingTheory/Valuation/RamificationGroup.lean