Commit 2025-01-27 01:57 77d9317d

View on Github →

chore(Algebra/Group/Submonoid/Operations): move instances to new file (#21067) Move declarations such as Submonoid.smul and Submonoid.mulAction into a new file, and shake some imports.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Group/Submonoid/MulAction.lean

added theorem Submonoid.mk_smul

added theorem Submonoid.smul_def

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

deleted theorem Submonoid.mk_smul

deleted theorem Submonoid.smul_def

Modified Mathlib/Algebra/Module/Submodule/Defs.lean

Modified Mathlib/Algebra/Polynomial/Basic.lean

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

Modified Mathlib/GroupTheory/MonoidLocalization/Basic.lean

Modified Mathlib/GroupTheory/OreLocalization/Basic.lean

Modified Mathlib/Topology/Algebra/Monoid.lean