Theorem exists_smul_not_mem_of_subset_orbit_closure

Modification history

2025-05-25 12:30
Mathlib/GroupTheory/Perm/ClosureSwap.lean
chore(*): not_mem/nmem -> notMem (#25159)
Deleted exists_smul_not_mem_of_subset_orbit_closureView on Github →
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 exists_smul_not_mem_of_subset_orbit_closureView on Github →