orderOf_mul_dvd_mul_orderOf — Mathlib

English

If x and y commute, then the order of x y divides the product orderOf(x) · orderOf(y).

Русский

Если x и y commuting, то orderOf(x y) делит произведение orderOf(x) и orderOf(y).

LaTeX

$$$\operatorname{orderOf}(x y) \mid \operatorname{orderOf}(x) \cdot \operatorname{orderOf}(y)$$$

Lean4

@[to_additive addOrderOf_add_dvd_mul_addOrderOf]
theorem orderOf_mul_dvd_mul_orderOf (h : Commute x y) : orderOf (x * y) ∣ orderOf x * orderOf y :=
  dvd_trans h.orderOf_mul_dvd_lcm (lcm_dvd_mul _ _)

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