Commit 2024-02-24 12:06 d6542aa5

View on Github →

feat(GroupTheory/Perm/ClosureSwap): A transitive permutation group generated by transpositions must be the whole symmetric group (#10035) This PR proves that a transitive permutation group generated by transpositions must be the whole symmetric group.

Estimated changes

Modified Mathlib.lean

Created Mathlib/GroupTheory/Perm/ClosureSwap.lean

added theorem Equiv.Perm.IsSwap.finite_compl_fixedBy

added theorem SubmonoidClass.swap_mem_trans

added theorem closure_of_isSwap_of_isPretransitive

added theorem exists_smul_not_mem_of_subset_orbit_closure

added theorem finite_compl_fixedBy_closure_iff

added theorem finite_compl_fixedBy_swap

added theorem mem_closure_isSwap'

added theorem mem_closure_isSwap

added theorem surjective_of_isSwap_of_isPretransitive

added theorem swap_mem_closure_isSwap