English
For any monoid α, minOrder α is defined as the infimum, in the extended natural order, of the orders of all non-identity elements that have finite order.
Русский
Для моноида α минимальный порядок — это инфimum порядков всех ненулевых элементов с конечным порядком.
LaTeX
$$$\minOrder(\alpha) = \inf\limits_{a\in \alpha, a\neq 1,\ IsOfFinOrder(a)}} \operatorname{order}(a)$$$
Lean4
/-- The minimum order of a non-identity element. Also the minimum size of a nontrivial subgroup, see
`Monoid.le_minOrder_iff_forall_subgroup`. Returns `∞` if the monoid is torsion-free. -/
@[to_additive /-- The minimum order of a non-identity element. Also the minimum size of a nontrivial
subgroup, see `AddMonoid.le_minOrder_iff_forall_addSubgroup`. Returns `∞` if the monoid is
torsion-free. -/
]
noncomputable def minOrder : ℕ∞ :=
⨅ (a : α) (_ha : a ≠ 1) (_ha' : IsOfFinOrder a), orderOf a
