Theorem Equiv.Perm.decomposeFin'_symm

Modification history

2026-08-27 12:57

Mathlib/GroupTheory/Perm/Fin.lean

feat(GroupTheory/Perm): another decomposition of permutations of `Fin (n + 2)` (#43168) …

Added Equiv.Perm.decomposeFin'_symm View on Github →