# Documentation

Mathlib.GroupTheory.Order.Min

# Minimum order of an element #

This file defines the minimum order of an element of a monoid.

## Main declarations #

• Monoid.minOrder: The minimum order of an element of a given monoid.
• Monoid.minOrder_eq_top: The minimum order is infinite iff the monoid is torsion-free.
• ZMod.minOrder: The minimum order of $$ℤ/nℤ$$ is the smallest factor of n, unless n = 0, 1.
noncomputable def AddMonoid.minOrder (α : Type u_1) [] :

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.

Equations
• = ⨅ (a : α), ⨅ (_ : a 0), ⨅ (_ : ), ()
Instances For
noncomputable def Monoid.minOrder (α : Type u_1) [] :

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.

Equations
• = ⨅ (a : α), ⨅ (_ : a 1), ⨅ (_ : ), ()
Instances For
@[simp]
theorem AddMonoid.minOrder_eq_top {α : Type u_1} [] :
@[simp]
theorem Monoid.minOrder_eq_top {α : Type u_1} [] :
@[simp]
theorem Monoid.IsTorsionFree.minOrder {α : Type u_1} [] :

Alias of the reverse direction of Monoid.minOrder_eq_top.

@[simp]
theorem AddMonoid.IsTorsionFree.minOrder {α : Type u_1} [] :
@[simp]
theorem AddMonoid.le_minOrder {α : Type u_1} [] {n : ℕ∞} :
∀ ⦃a : α⦄, a 0n ()
@[simp]
theorem Monoid.le_minOrder {α : Type u_1} [] {n : ℕ∞} :
∀ ⦃a : α⦄, a 1n ()
theorem AddMonoid.minOrder_le_addOrderOf {α : Type u_1} [] {a : α} (ha : a 0) (ha' : ) :
theorem Monoid.minOrder_le_orderOf {α : Type u_1} [] {a : α} (ha : a 1) (ha' : ) :
()