# Documentation

Mathlib.GroupTheory.Exponent

# Exponent of a group #

This file defines the exponent of a group, or more generally a monoid. For a group G it is defined to be the minimal n≥1 such that g ^ n = 1 for all g ∈ G. For a finite group G, it is equal to the lowest common multiple of the order of all elements of the group G.

## Main definitions #

• Monoid.ExponentExists is a predicate on a monoid G saying that there is some positive n such that g ^ n = 1 for all g ∈ G.
• Monoid.exponent defines the exponent of a monoid G as the minimal positive n such that g ^ n = 1 for all g ∈ G, by convention it is 0 if no such n exists.
• AddMonoid.ExponentExists the additive version of Monoid.ExponentExists.
• AddMonoid.exponent the additive version of Monoid.exponent.

## Main results #

• Monoid.lcm_order_eq_exponent: For a finite left cancel monoid G, the exponent is equal to the Finset.lcm of the order of its elements.
• Monoid.exponent_eq_iSup_orderOf('): For a commutative cancel monoid, the exponent is equal to ⨆ g : G, orderOf g (or zero if it has any order-zero elements).

## TODO #

• Refactor the characteristic of a ring to be the exponent of its underlying additive group.

A predicate on an additive monoid saying that there is a positive integer n such

that n • g = 0 for all g.

Instances For

A predicate on a monoid saying that there is a positive integer n such that g ^ n = 1 for all g.

Instances For
noncomputable def AddMonoid.exponent (G : Type u) [] :

The exponent of an additive group is the smallest positive integer n such that

n • g = 0 for all g ∈ G if it exists, otherwise it is zero by convention.

Instances For
noncomputable def Monoid.exponent (G : Type u) [] :

The exponent of a group is the smallest positive integer n such that g ^ n = 1 for all g ∈ G if it exists, otherwise it is zero by convention.

Instances For
(x : ) → ((n : ) → (hn : 0 < n) → (hgn : ∀ (g : G), n g = 0) → motive (_ : n, 0 < n ∀ (g : G), n g = 0)) → motive x
Instances For
theorem AddMonoid.exponent_eq_zero_addOrder_zero {G : Type u} [] {g : G} (hg : = 0) :
theorem Monoid.exponent_eq_zero_of_order_zero {G : Type u} [] {g : G} (hg : = 0) :
theorem AddMonoid.exponent_nsmul_eq_zero {G : Type u} [] (g : G) :
= 0
theorem Monoid.pow_exponent_eq_one {G : Type u} [] (g : G) :
= 1
theorem AddMonoid.nsmul_eq_mod_exponent {G : Type u} [] {n : } (g : G) :
n g = () g
theorem Monoid.pow_eq_mod_exponent {G : Type u} [] {n : } (g : G) :
g ^ n = g ^ ()
theorem AddMonoid.exponent_pos_of_exists {G : Type u} [] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), n g = 0) :
theorem Monoid.exponent_pos_of_exists {G : Type u} [] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) :
theorem AddMonoid.exponent_min' {G : Type u} [] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), n g = 0) :
theorem Monoid.exponent_min' {G : Type u} [] (n : ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) :
theorem AddMonoid.exponent_min {G : Type u} [] (m : ) (hpos : 0 < m) (hm : ) :
g, m g 0
theorem Monoid.exponent_min {G : Type u} [] (m : ) (hpos : 0 < m) (hm : ) :
g, g ^ m 1
@[simp]
@[simp]
theorem Monoid.exp_eq_one_of_subsingleton {G : Type u} [] [] :
theorem Monoid.order_dvd_exponent {G : Type u} [] (g : G) :
theorem AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero (G : Type u_1) [] (n : ) (hG : ∀ (g : G), n g = 0) :
theorem Monoid.exponent_dvd_of_forall_pow_eq_one (G : Type u_1) [] (n : ) (hG : ∀ (g : G), g ^ n = 1) :
theorem Monoid.lcm_orderOf_dvd_exponent (G : Type u) [] [] :
Finset.lcm Finset.univ orderOf
g, = p ^ ↑() p
theorem Nat.Prime.exists_orderOf_eq_pow_factorization_exponent (G : Type u) [] {p : } (hp : ) :
g, = p ^ ↑() p
theorem AddMonoid.exponent_ne_zero_iff_range_addOrderOf_finite {G : Type u} [] (h : ∀ (g : G), 0 < ) :
theorem Monoid.exponent_ne_zero_iff_range_orderOf_finite {G : Type u} [] (h : ∀ (g : G), 0 < ) :
theorem AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite {G : Type u} [] (h : ∀ (g : G), 0 < ) :
theorem Monoid.exponent_eq_zero_iff_range_orderOf_infinite {G : Type u} [] (h : ∀ (g : G), 0 < ) :
theorem Monoid.lcm_order_eq_exponent {G : Type u} [] [] :
Finset.lcm Finset.univ orderOf =
theorem AddMonoid.exponent_eq_iSup_addOrderOf {G : Type u} [] (h : ∀ (g : G), 0 < ) :
= ⨆ (g : G),
theorem Monoid.exponent_eq_iSup_orderOf {G : Type u} [] (h : ∀ (g : G), 0 < ) :
= ⨆ (g : G),