Commit 2024-08-13 08:09 ee3fc238

View on Github →

chore(Algebra/Group/Aut): Do not import MonoidWithZero (#15430) Move what needs it to a new file Algebra.GroupWithZero.Action.Basic which will eventually contain more content coming from Algebra.SMulWithZero.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/Aut.lean

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

added def DistribMulAction.toAddAut

added def DistribMulAction.toAddEquiv

added theorem IsUnit.smul_sub_iff_sub_inv_smul

added def MulDistribMulAction.toMulAut

added def MulDistribMulAction.toMulEquiv

added def arrowMulDistribMulAction

added def mulAutArrow

added def smulMonoidWithZeroHom

Modified Mathlib/Algebra/Module/Equiv/Basic.lean

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

Modified Mathlib/Algebra/Ring/AddAut.lean

Modified Mathlib/Algebra/SMulWithZero.lean

deleted def smulMonoidWithZeroHom

Modified Mathlib/Data/DFinsupp/Basic.lean

Modified Mathlib/Data/Set/Pointwise/SMul.lean

Modified Mathlib/GroupTheory/GroupAction/Group.lean

deleted def DistribMulAction.toAddAut

deleted def DistribMulAction.toAddEquiv

deleted theorem IsUnit.smul_sub_iff_sub_inv_smul

deleted def MulDistribMulAction.toMulAut

deleted def MulDistribMulAction.toMulEquiv

deleted def arrowMulDistribMulAction

deleted def mulAutArrow

Modified Mathlib/RingTheory/Nilpotent/Basic.lean