Commit 2025-06-15 08:42 5f1d6fc9

View on Github →

feat(GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup): action of the fixing Subgroup on the complement of a set (#23970) Introduce the SubMulAction of a fixingSubgroup of a subset on the complement of that set. Develop relations between these and SubMulAction of stabilizers.

Estimated changes

Modified Mathlib.lean

Modified Mathlib/Algebra/Group/End.lean

Modified Mathlib/GroupTheory/GroupAction/FixingSubgroup.lean

Modified Mathlib/GroupTheory/GroupAction/MultipleTransitivity.lean

added theorem SubMulAction.ofFixingSubgroup.isMultiplyPretransitive'

added theorem SubMulAction.ofFixingSubgroup.isMultiplyPretransitive

Modified Mathlib/GroupTheory/GroupAction/SubMulAction.lean

modified theorem SubMulAction.compl_def

Created Mathlib/GroupTheory/GroupAction/SubMulAction/OfFixingSubgroup.lean

added theorem Set.conj_mem_fixingSubgroup

added def SubMulAction.conjMap_ofFixingSubgroup

added theorem SubMulAction.conjMap_ofFixingSubgroup_bijective

added theorem SubMulAction.conjMap_ofFixingSubgroup_coe_apply

added def SubMulAction.fixingSubgroupEquivFixingSubgroup

added theorem SubMulAction.fixingSubgroupEquivFixingSubgroup_coe_apply

added def SubMulAction.fixingSubgroupInsertEquiv

added theorem SubMulAction.fixingSubgroup_map_conj_eq

added theorem SubMulAction.fixingSubgroup_of_insert

added theorem SubMulAction.fixingSubgroup_smul_eq_fixingSubgroup_map_conj

added def SubMulAction.map_ofFixingSubgroupUnion

added theorem SubMulAction.map_ofFixingSubgroupUnion_bijective

added theorem SubMulAction.map_ofFixingSubgroupUnion_def

added theorem SubMulAction.mem_fixingSubgroup_insert_iff

added theorem SubMulAction.mem_ofFixingSubgroup_iff

added theorem SubMulAction.mem_ofFixingSubgroup_insert_iff

added theorem SubMulAction.not_mem_of_mem_ofFixingSubgroup

added theorem SubMulAction.ofFixingSubgroup.append_left

added theorem SubMulAction.ofFixingSubgroup.append_right

added def SubMulAction.ofFixingSubgroup

added theorem SubMulAction.ofFixingSubgroupEmpty_equivariantMap_bijective

added theorem SubMulAction.ofFixingSubgroup_carrier

added def SubMulAction.ofFixingSubgroup_equivariantMap

added theorem SubMulAction.ofFixingSubgroup_equivariantMap_injective

added def SubMulAction.ofFixingSubgroup_insert_map

added theorem SubMulAction.ofFixingSubgroup_insert_map_apply

added theorem SubMulAction.ofFixingSubgroup_insert_map_bijective

added def SubMulAction.ofFixingSubgroup_of_eq

added theorem SubMulAction.ofFixingSubgroup_of_eq_apply

added theorem SubMulAction.ofFixingSubgroup_of_eq_bijective

added def SubMulAction.ofFixingSubgroup_of_inclusion

added theorem SubMulAction.ofFixingSubgroup_of_inclusion_injective

added def SubMulAction.ofFixingSubgroup_of_singleton

added theorem SubMulAction.ofFixingSubgroup_of_singleton_bijective

added theorem SubMulAction.of_fixingSubgroupEmpty_mapScalars_surjective