English
If x and y commute, then the order of y divides the lcm of the orders of x and of x y.
Русский
Если x и y commute, то порядок y делит наибольший общий кратный порядков x и x y.
LaTeX
$$$\operatorname{orderOf}(y) \mid \operatorname{lcm}(\operatorname{orderOf}(x), \operatorname{orderOf}(x y))$$$
Lean4
@[to_additive]
theorem orderOf_dvd_lcm_mul (h : Commute x y) : orderOf y ∣ Nat.lcm (orderOf x) (orderOf (x * y)) :=
by
by_cases h0 : orderOf x = 0
· rw [h0, lcm_zero_left]
apply dvd_zero
conv_lhs =>
rw [← one_mul y, ← pow_orderOf_eq_one x, ← succ_pred_eq_of_pos (Nat.pos_of_ne_zero h0), _root_.pow_succ, mul_assoc]
exact
(((Commute.refl x).mul_right h).pow_left _).orderOf_mul_dvd_lcm.trans
(lcm_dvd_iff.2 ⟨(orderOf_pow_dvd _).trans (dvd_lcm_left _ _), dvd_lcm_right _ _⟩)
