Theorem surjective_of_isSwap_of_isPretransitive'

Modification history

2025-11-20 16:02
Mathlib/GroupTheory/Perm/ClosureSwap.lean
feat(GroupTheory/Perm/ClosureSwap): add slight generalization (#31570) …
Added surjective_of_isSwap_of_isPretransitive'View on Github →