Commit 2025-03-04 10:47 1fd89433

View on Github →

chore(GroupTheory/GroupAction/Defs): don't import DistribMulAction (#22512) This is a ring-like action, while this file is about group-like objects. See #10043 for the new Algebra.Ring.Action.Submonoid copyright header.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Ring/Action/Submonoid.lean

added def FixedPoints.addSubgroup

added theorem FixedPoints.addSubgroup_toAddSubmonoid

added def FixedPoints.addSubmonoid

added theorem FixedPoints.mem_addSubgroup

added theorem FixedPoints.mem_addSubmonoid

Modified Mathlib/GroupTheory/GroupAction/Defs.lean

deleted def FixedPoints.addSubgroup

deleted theorem FixedPoints.addSubgroup_toAddSubmonoid

deleted def FixedPoints.addSubmonoid

deleted theorem FixedPoints.mem_addSubgroup

deleted theorem FixedPoints.mem_addSubmonoid