English
The order of x is the least positive n with x^n = 1, or 0 if no such n exists.
Русский
Порядок элемента x — это наименьшее положительное n такое, что x^n = 1; если такого n нет, порядок равен 0.
LaTeX
$$orderOf(x) = 0 \\iff x\\text{ имеет бесконечный порядок};\\quad orderOf(x) = \\min\\{n \\ge 1 : x^n = 1\\}\\text{ если существует }$$
Lean4
/-- `orderOf x` is the order of the element `x`, i.e. the `n ≥ 1`, s.t. `x ^ n = 1` if it exists.
Otherwise, i.e. if `x` is of infinite order, then `orderOf x` is `0` by convention. -/
@[to_additive /-- `addOrderOf a` is the order of the element `a`, i.e. the `n ≥ 1`, s.t. `n • a = 0` if it
exists. Otherwise, i.e. if `a` is of infinite order, then `addOrderOf a` is `0` by convention. -/
]
noncomputable def orderOf (x : G) : ℕ :=
minimalPeriod (x * ·) 1
