orderOf_mul_eq_mul_orderOf_of_coprime

English

If x and y commute and their orders are coprime, then the order of x y equals the product of their orders.

Русский

Если x и y commute и их порядки взаимно просты, то orderOf(x y) = orderOf(x) · orderOf(y).

LaTeX

$$\operatorname{orderOf}(x y) = \operatorname{orderOf}(x) \cdot \operatorname{orderOf}(y) \quad\text{when } \operatorname{Coprime}(\operatorname{orderOf}(x), \operatorname{orderOf}(y))$$

Lean4

@[to_additive addOrderOf_add_eq_mul_addOrderOf_of_coprime]
theorem orderOf_mul_eq_mul_orderOf_of_coprime (h : Commute x y) (hco : (orderOf x).Coprime (orderOf y)) :
    orderOf (x * y) = orderOf x * orderOf y :=
  by
  rw [orderOf, ← comp_mul_left]
  exact h.function_commute_mul_left.minimalPeriod_of_comp_eq_mul_of_coprime hco

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