isOfFinOrder_mul — Mathlib

English

If x and y commute and each has finite order, then x y has finite order.

Русский

Если x и y commute и оба имеют конечный порядок, то x y имеет конечный порядок.

LaTeX

$$\operatorname{IsOfFinOrder}(x) \land \operatorname{IsOfFinOrder}(y) \Rightarrow \operatorname{IsOfFinOrder}(x y)$$

Lean4

/-- Commuting elements of finite order are closed under multiplication. -/
@[to_additive /-- Commuting elements of finite additive order are closed under addition. -/
    ]
theorem isOfFinOrder_mul (h : Commute x y) (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) : IsOfFinOrder (x * y) :=
  orderOf_pos_iff.mp <| pos_of_dvd_of_pos h.orderOf_mul_dvd_mul_orderOf <| mul_pos hx.orderOf_pos hy.orderOf_pos

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