Commit 2025-06-27 03:35 4198e49f
View on Github →feat: Multiple Primitivity of group actions (#26279)
An action of a group G on a type X is n-primitive if it is n-transitive and if,
for every subset s of cardinality n of X, the action of fixingSubgroup G s on the complement of s is primitive.
This PR develops the basics of this notion.
This PR continues the work from #23979.
Original PR: https://github.com/leanprover-community/mathlib4/pull/23979