sign): Add `equiv.perm.move`, to move an item in a permutation

Commit

5 years ago

feat(group_theory/perm/sign): Add `equiv.perm.move`, to move an item in a permutation Also provides a decomposition to convert any swap into a series of adjacent swaps

References

#4739 - feat(group_theory/perm/sign): Add `equiv.perm.move`, to move an item in a permutation

Author

eric-wieser

Committer

eric-wieser

Parents

cac45580

mathlib 1c13a10c - feat(group_theory/perm/sign): Add `equiv.perm.move`, to move an item in a permutation

mathlib
1c13a10c - feat(group_theory/perm/sign): Add `equiv.perm.move`, to move an item in a permutation