Commit 2025-12-01 10:02 311ef188
View on Github →feat(GroupTheory/GroupAction/SubMulAction/Combination): combinations and group actions (#27107)
Nat.Combination X n is the type all s : Finset X such that s.card = n.
This PR provides some API for this subtype and the SubMulAction it inherits when a group acts on X.
It will be used in conjunction with the description of some maximal subgroups of Equiv.Perm X to construct primitive actions.
Question on the names: when X is a fintype, there is Finset.powersetCard that gives the same object, as a Finset. But the present PR also applies when X is infinite. Then maybe Nat.Combination should be renamed as Set.powersetCard?