Commit 2024-02-01 11:35 2bbb174e

View on Github →

feat(GroupTheory/GroupAction/Basic): define subgroups fixed by group actions (#10043)

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

added def FixedPoints.addSubgroup

added theorem FixedPoints.addSubgroup_toAddSubmonoid

added def FixedPoints.addSubmonoid

added theorem FixedPoints.mem_addSubgroup

added theorem FixedPoints.mem_addSubmonoid

added theorem FixedPoints.mem_subgroup

added theorem FixedPoints.mem_submonoid

added def FixedPoints.subgroup

added theorem FixedPoints.subgroup_toSubmonoid

added def FixedPoints.submonoid