prod_mk — Mathlib

English

If a has finite order and b has finite order, then (a, b) has finite order.

Русский

Если у a и b конечный порядок, то у пары (a, b) также конечный порядок.

LaTeX

$$($\operatorname{FinOrd}(a) \land \operatorname{FinOrd}(b)$) ⇒ \operatorname{FinOrd}((a,b))$$

Lean4

@[to_additive IsOfFinAddOrder.prod_mk]
theorem prod_mk : IsOfFinOrder a → IsOfFinOrder b → IsOfFinOrder (a, b) := by
  simpa only [← orderOf_pos_iff, Prod.orderOf] using Nat.lcm_pos

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