Theorem Equiv.Perm.decomposeFin'Symm_symm_succAbove

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_symm_succAboveView on Github →