Composite_of_Permutations_is_Permutation
Provedpermutation-theoryproofwiki
Let f, g be permutations of a set S. Then their composite g ∘ f is also a permutation of S.
Preamble
import Mathlib.GroupTheory.Perm.Basic
Formal statement
theorem Composite_of_Permutations_is_Permutation {α : Type _} (f g : Equiv.Perm α) : ∃ h : Equiv.Perm α, (h : α → α) = (f : α → α) ∘ (g : α → α) := by sorrySource