Commit 2026-02-02 08:05 51da7e3f

View on Github →

feat(GroupTheory/GroupAction/SubMulAction/Combination): primitivity of the permutation action. (#34307) Prove the primitivity of the permutation action of Equiv.Perm or alternatingGroup on Nat.Combination. This will be used in #33082 to prove the simplicity of the alternating group on at least 5 letters.

Estimated changes

Modified Mathlib/GroupTheory/GroupAction/SubMulAction/Combination.lean

modified theorem Set.powersetCard.addAction_faithful

added theorem Set.powersetCard.card_eq

modified theorem Set.powersetCard.coe_coe

modified theorem Set.powersetCard.coe_compl

added theorem Set.powersetCard.coe_finset

modified theorem Set.powersetCard.coe_mulActionHom_of_embedding

added theorem Set.powersetCard.coe_nonempty_iff

added theorem Set.powersetCard.coe_nontrivial_iff

modified theorem Set.powersetCard.coe_smul

modified def Set.powersetCard.compl

added theorem Set.powersetCard.eq_empty_iff

modified theorem Set.powersetCard.faithfulSMul

modified theorem Set.powersetCard.faithfulVAdd

added theorem Set.powersetCard.infinite

added theorem Set.powersetCard.isPreprimitive_alternatingGroup

added theorem Set.powersetCard.isPreprimitive_perm

modified theorem Set.powersetCard.isPretransitive

added theorem Set.powersetCard.isPretransitive_alternatingGroup

modified theorem Set.powersetCard.mem_compl

modified def Set.powersetCard.mulActionHom_of_embedding

modified theorem Set.powersetCard.mulActionHom_of_embedding_surjective

modified def Set.powersetCard.mulActionHom_singleton

modified theorem Set.powersetCard.mulActionHom_singleton_bijective

modified theorem Set.powersetCard.mulAction_faithful

added theorem Set.powersetCard.ncard_eq

added theorem Set.powersetCard.nontrivial_iff

added theorem Set.powersetCard.stabilizer_coe

modified def Set.powersetCard.subMulAction