IsOfFinOrder — Mathlib

English

IsOfFinOrder is defined as x having a finite order in a monoid: there exists n ≥ 1 with x^n = 1.

Русский

IsOfFinOrder определяется как существование конечного порядка: ∃ n ≥ 1: x^n = 1.

LaTeX

$$$\IsOfFinOrder(x) \equiv ∃ n \ge 1, x^n = 1$$$

Lean4

/-- `IsOfFinOrder` is a predicate on an element `x` of a monoid to be of finite order, i.e. there
exists `n ≥ 1` such that `x ^ n = 1`. -/
@[to_additive /-- `IsOfFinAddOrder` is a predicate on an element `a` of an
    additive monoid to be of finite order, i.e. there exists `n ≥ 1` such that `n • a = 0`. -/
    ]
def IsOfFinOrder (x : G) : Prop :=
  (1 : G) ∈ periodicPts (x * ·)

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