Commit 2025-03-03 13:51 6d4818e4

View on Github →

chore: move MulDistribMulAction material earlier (#22121)

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/AddTorsor/Defs.lean

Modified Mathlib/Algebra/Field/Action/ConjAct.lean

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

added def arrowMulDistribMulAction

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

added def MulDistribMulAction.toMulAut

added def mulAutArrow

Modified Mathlib/Algebra/Group/Pointwise/Set/Finite.lean

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

deleted def MulDistribMulAction.toMulAut

deleted def arrowMulDistribMulAction

deleted def mulAutArrow

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

added def Subgroup.centerUnitsEquivUnitsCenter

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

Modified Mathlib/GroupTheory/GroupAction/ConjAct.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

Modified Mathlib/GroupTheory/GroupAction/Embedding.lean

Modified Mathlib/GroupTheory/GroupAction/Support.lean

Modified Mathlib/GroupTheory/Subgroup/Center.lean

deleted def Subgroup.centerUnitsEquivUnitsCenter

Modified Mathlib/GroupTheory/Subgroup/Centralizer.lean

Modified Mathlib/LinearAlgebra/AffineSpace/Defs.lean

Modified Mathlib/RingTheory/LittleWedderburn.lean