Order_of_Product_of_Disjoint_Permutations_v2
Proveddisjointgroup-theoryorderpermutationsproofwiki
Let denote the symmetric group on letters. Let be a product of disjoint permutations of orders . Then where denotes the order of in denotes lowest common multiple.
Preamble
import Mathlib.Analysis.Complex.Basic import Mathlib.GroupTheory.Perm.Cycle.Type
Formal statement
theorem Order_of_Product_of_Disjoint_Permutations_v2 {α : Type _} [DecidableEq α] [Fintype α] (σ τ : Equiv.Perm α) (h : Equiv.Perm.Disjoint σ τ) : orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) := by sorrySource