Commit 2025-07-10 04:21 55b8498c

feat(GroupTheory/GroupAction/MultiplyPretransitive) : Multiple transivity property of the permutation group (#26281)

• The permutation group is pretransitive, is multiply pretransitive, and is preprimitive (for its natural action)
• Equiv.Perm.eq_top_if_isMultiplyPretransitive: a subgroup of Equiv.Perm α which is Nat.card α - 1 pretransitive is equal to ⊤. This PR continues the work from #24130 Original PR: https://github.com/leanprover-community/mathlib4/pull/24130

• depends on: #26280
• depends on: #26279