Commit 2026-08-27 12:57 aa28759c

feat(GroupTheory/Perm): another decomposition of permutations of Fin (n + 2) (#43168) We introduce another decomposition def Equiv.Perm.decomposeFin' (n : ℕ) : Perm (Fin (n + 2)) ≃ Fin (n + 2) × Perm (Fin (n + 1)). The inverse map sends ⟨i, σ⟩ (with i : Fin (n + 2) and σ : Perm (Fin (n + 1)) to the permutation which sends 0 to i and j.succ to i.succAbove (σ j). This shall be used in the study of the subdivision operator on singular chains (which involves an induction on n). From https://github.com/joelriou/excision