orderOf_pos_iff — Mathlib

English

0 < orderOf x iff IsOfFinOrder x.

Русский

0 < orderOf x эквивалентно конечному порядку x.

LaTeX

$$0 < orderOf x \\iff IsOfFinOrder x$$

Lean4

/-- A group element has finite order iff its order is positive. -/
@[to_additive (attr := simp) /-- A group element has finite additive order iff its order is positive. -/
    ]
theorem orderOf_pos_iff : 0 < orderOf x ↔ IsOfFinOrder x := by rw [iff_not_comm.mp orderOf_eq_zero_iff, pos_iff_ne_zero]

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