English
If two permutations σ and τ have disjoint supports, then the order of their product equals the least common multiple of their orders: order(σ τ) = lcm(order(σ), order(τ)).
Русский
Если две перестановки σ и τ имеют несмешивающиеся поддержки, то порядок их произведения равен наименьшему общему кратному порядков σ и порядков τ: order(στ) = lcm(order(σ), order(τ)).
LaTeX
$$$\\operatorname{order}(\\sigma \\tau) = \\operatorname{lcm}(\\operatorname{order}(\\sigma), \\operatorname{order}(\\tau)).$$$
Lean4
nonrec theorem orderOf {σ τ : Perm α} (hστ : Disjoint σ τ) : orderOf (σ * τ) = Nat.lcm (orderOf σ) (orderOf τ) :=
haveI h : ∀ n : ℕ, (σ * τ) ^ n = 1 ↔ σ ^ n = 1 ∧ τ ^ n = 1 := fun n => by
rw [hστ.commute.mul_pow, Disjoint.mul_eq_one_iff (hστ.pow_disjoint_pow n n)]
Nat.dvd_antisymm hστ.commute.orderOf_mul_dvd_lcm
(Nat.lcm_dvd (orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).1)
(orderOf_dvd_of_pow_eq_one ((h (orderOf (σ * τ))).mp (pow_orderOf_eq_one (σ * τ))).2))
