Commit 2023-01-27 14:47 bba03a92

View on Github →

feat: Port/GroupTheory.GroupAction.FixingSubgroup (#1868) port of group_theory.group_action.fixing_subgroup

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean

added theorem fixedPoints_antitone

added theorem fixedPoints_subgroup_antitone

added theorem fixedPoints_subgroup_sup

added theorem fixedPoints_subgroup_supᵢ

added theorem fixedPoints_submonoid_sup

added theorem fixedPoints_submonoid_supᵢ

added def fixingSubgroup

added theorem fixingSubgroup_antitone

added theorem fixingSubgroup_fixedPoints_gc

added theorem fixingSubgroup_union

added theorem fixingSubgroup_unionᵢ

added def fixingSubmonoid

added theorem fixingSubmonoid_antitone

added theorem fixingSubmonoid_fixedPoints_gc

added theorem fixingSubmonoid_union

added theorem fixingSubmonoid_unionᵢ

added theorem mem_fixingSubgroup_iff

added theorem mem_fixingSubmonoid_iff