Splitting a multiset along a fixed-point-free involution

A multiset invariant under a fixed-point-free involution τ splits as N + N.map τ.

Auxiliary material for the formalization of M. Stoll, Galois groups over ℚ of some iterated polynomials, Arch. Math. 59 (1992), 239-244; upstreaming candidates for Mathlib.

theorem Multiset.exists_add_map_of_involutive {β : Type u_1} (τ : β → β) (M : Multiset β) (hτ : ∀ (x : β), x ∈ M → τ (τ x) = x) (hinv : map τ M = M) (hfix : ∀ (x : β), x ∈ M → τ x ≠ x) : ∃ (N : Multiset β), M = N + map τ N

A multiset M invariant under an involution τ that is fixed-point-free on its support splits as N + N.map τ.