Theorems · Definition · group theory

orderOf

{G : Type u_1} → [Monoid G] → G → ℕ

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.

Defined in

Mathlib.GroupTheory.OrderOfElement

Cited by

324 results in Mathlib

Foundations

Depth 19 from the axioms, rests on 186 definitions · uses propext, Classical.choice, Quot.sound

Assumes

Monoid