Theorem Equiv.Perm.decomposeFin'Symm_uncurry_bijective

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