Theorem exists_smul_notMem_of_subset_orbit_closure

Modification history

2025-05-25 12:30
Mathlib/GroupTheory/Perm/ClosureSwap.lean
chore(*): not_mem/nmem -> notMem (#25159)
Added exists_smul_notMem_of_subset_orbit_closureView on Github →