Commit 2023-12-22 20:03 07756d1c

View on Github →

feat: Stabilizers of sets/finsets (#8924) Prove a bunch of results about stabilizer G s where Group G, MulAction G α, s : Set α.

Estimated changes

Modified Mathlib.lean

Created Mathlib/Algebra/Pointwise/Stabilizer.lean

added theorem MulAction.map_stabilizer_le

added theorem MulAction.mem_stabilizer_finset'

added theorem MulAction.mem_stabilizer_finset

added theorem MulAction.mem_stabilizer_finset_iff_smul_finset_subset

added theorem MulAction.mem_stabilizer_finset_iff_subset_smul_finset

added theorem MulAction.mem_stabilizer_set'

added theorem MulAction.mem_stabilizer_set

added theorem MulAction.mem_stabilizer_set_iff_smul_set_subset

added theorem MulAction.mem_stabilizer_set_iff_subset_smul_set

added theorem MulAction.mul_stabilizer_self

added theorem MulAction.stabilizer_coe_finset

added theorem MulAction.stabilizer_empty

added theorem MulAction.stabilizer_finset_empty

added theorem MulAction.stabilizer_finset_singleton

added theorem MulAction.stabilizer_image_coe_quotient

added theorem MulAction.stabilizer_mul_self

added theorem MulAction.stabilizer_op_subgroup

added theorem MulAction.stabilizer_singleton

added theorem MulAction.stabilizer_subgroup

added theorem MulAction.stabilizer_subgroup_op

Modified Mathlib/GroupTheory/GroupAction/Basic.lean

added theorem MulAction.le_stabilizer_smul_left

added theorem MulAction.le_stabilizer_smul_right

added theorem MulAction.stabilizer_mul_eq_left

added theorem MulAction.stabilizer_mul_eq_right

added theorem MulAction.stabilizer_smul_eq_left

added theorem MulAction.stabilizer_smul_eq_right

Modified Mathlib/GroupTheory/QuotientGroup.lean

added theorem QuotientGroup.image_coe

added theorem QuotientGroup.image_coe_inj

added theorem QuotientGroup.map_mk'_self

added theorem QuotientGroup.preimage_image_coe