English
If x and y commute and have nonzero orders, the order of a suitably constructed product equals the least common multiple of their orders.
Русский
Пусть x и y коммутируют и их порядки ненулевые; тогда порядок элемента, построенного как произведение этих степеней, равен НОК их порядков.
LaTeX
$$$\\\\operatorname{orderOf}\\bigl(x^{\\\\frac{\\\\operatorname{orderOf} x}{\\\\operatorname{factorizationLCMLeft}(\\\\operatorname{orderOf} x)(\\\\operatorname{orderOf} y)} } \\, * \\, y^{\\\\frac{\\\\operatorname{orderOf} y}{\\\\operatorname{factorizationLCMRight}(\\\\operatorname{orderOf} x)(\\\\operatorname{orderOf} y)} }\\\\bigr) = \\\\operatorname{lcm}(\\\\operatorname{orderOf} x, \\\\operatorname{orderOf} y)$$$
Lean4
/-- If two commuting elements `x` and `y` of a monoid have order `n` and `m`, there is an element
of order `lcm n m`. The result actually gives an explicit (computable) element, written as the
product of a power of `x` and a power of `y`. See also the result below if you don't need the
explicit formula. -/
@[to_additive /-- If two commuting elements `x` and `y` of an additive monoid have order `n` and
`m`, there is an element of order `lcm n m`. The result actually gives an explicit (computable)
element, written as the sum of a multiple of `x` and a multiple of `y`. See also the result below
if you don't need the explicit formula. -/
]
theorem _root_.Commute.orderOf_mul_pow_eq_lcm {x y : G} (h : Commute x y) (hx : orderOf x ≠ 0) (hy : orderOf y ≠ 0) :
orderOf
(x ^ (orderOf x / (factorizationLCMLeft (orderOf x) (orderOf y))) *
y ^ (orderOf y / factorizationLCMRight (orderOf x) (orderOf y))) =
Nat.lcm (orderOf x) (orderOf y) :=
by
rw [(h.pow_pow _ _).orderOf_mul_eq_mul_orderOf_of_coprime]
all_goals iterate 2 rw [orderOf_pow_orderOf_div]; try rw [Coprime]
all_goals
simp [factorizationLCMLeft_mul_factorizationLCMRight, factorizationLCMLeft_dvd_left,
factorizationLCMRight_dvd_right, coprime_factorizationLCMLeft_factorizationLCMRight, hx, hy]
