Theorem Equiv.Perm.IsSwap.finite_compl_fixedBy

Modification history

2024-02-24 12:06
Mathlib/GroupTheory/Perm/ClosureSwap.lean
feat(GroupTheory/Perm/ClosureSwap): A transitive permutation group generated by transpositions must be the whole symmetric group (#10035) …
Added Equiv.Perm.IsSwap.finite_compl_fixedByView on Github →