mul — Mathlib

English

In a commutative monoid, the product of two finite-order elements has finite order.

Русский

В коммутативном моноиде произведение двух элементов конечного порядка имеет конечный порядок.

LaTeX

$$IsOfFinOrder x → IsOfFinOrder y → IsOfFinOrder (x*y)$$

Lean4

/-- Elements of finite order are closed under multiplication. -/
@[to_additive /-- Elements of finite additive order are closed under addition. -/
    ]
theorem mul (hx : IsOfFinOrder x) (hy : IsOfFinOrder y) : IsOfFinOrder (x * y) :=
  (Commute.all x y).isOfFinOrder_mul hx hy

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