English
For a finite left-cancellative monoid G and any x ∈ G, the order of x is positive: 0 < orderOf x.
Русский
Для конечного левоотменяющего моноида G и любого x ∈ G порядок x положителен: 0 < orderOf x.
LaTeX
$$$0 < \operatorname{orderOf}(x)$$$
Lean4
/-- This is the same as `IsOfFinOrder.orderOf_pos` but with one fewer explicit assumption since this
is automatic in case of a finite cancellative monoid. -/
@[to_additive /-- This is the same as `IsOfFinAddOrder.addOrderOf_pos` but with one fewer explicit
assumption since this is automatic in case of a finite cancellative additive monoid. -/
]
theorem orderOf_pos (x : G) : 0 < orderOf x :=
(isOfFinOrder_of_finite x).orderOf_pos
