orderOf_mul_dvd_lcm — Mathlib

English

If x and y commute, then the order of the product x y divides the least common multiple of the orders of x and y.

Русский

Если элементы x и y commute, то порядок произведения x y делит наименьшее общее кратное порядков x и y.

LaTeX

$$$\operatorname{orderOf}(x y) \mid \operatorname{lcm}(\operatorname{orderOf}(x), \operatorname{orderOf}(y))$$$

Lean4

@[to_additive]
theorem orderOf_mul_dvd_lcm (h : Commute x y) : orderOf (x * y) ∣ Nat.lcm (orderOf x) (orderOf y) :=
  by
  rw [orderOf, ← comp_mul_left]
  exact Function.Commute.minimalPeriod_of_comp_dvd_lcm h.function_commute_mul_left

Похожие утверждения