# mathlib3documentation

group_theory.exponent

# Exponent of a group #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.exponent_exists 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.
• add_monoid.exponent_exists the additive version of monoid.exponent_exists.
• add_monoid.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_supr_order_of('): For a commutative cancel monoid, the exponent is equal to ⨆ g : G, order_of 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.
Prop

A predicate on an additive monoid saying that there is a positive integer n such that n • g = 0 for all g.

Equations
def monoid.exponent_exists (G : Type u) [monoid G] :
Prop

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

Equations
noncomputable def monoid.exponent (G : Type u) [monoid G] :

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.

Equations

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.

Equations
theorem add_monoid.exponent_eq_zero_of_order_zero {G : Type u} [add_monoid G] {g : G} (hg : = 0) :
theorem monoid.exponent_eq_zero_of_order_zero {G : Type u} [monoid G] {g : G} (hg : = 0) :
theorem monoid.pow_exponent_eq_one {G : Type u} [monoid G] (g : G) :
= 1
theorem add_monoid.exponent_nsmul_eq_zero {G : Type u} [add_monoid G] (g : G) :
= 0
theorem add_monoid.nsmul_eq_mod_exponent {G : Type u} [add_monoid G] {n : } (g : G) :
n g = (n % g
theorem monoid.pow_eq_mod_exponent {G : Type u} [monoid G] {n : } (g : G) :
g ^ n = g ^ (n %
theorem monoid.exponent_pos_of_exists {G : Type u} [monoid G] (n : ) (hpos : 0 < n) (hG : (g : G), g ^ n = 1) :
theorem add_monoid.exponent_pos_of_exists {G : Type u} [add_monoid G] (n : ) (hpos : 0 < n) (hG : (g : G), n g = 0) :
theorem monoid.exponent_min' {G : Type u} [monoid G] (n : ) (hpos : 0 < n) (hG : (g : G), g ^ n = 1) :
theorem add_monoid.exponent_min' {G : Type u} [add_monoid G] (n : ) (hpos : 0 < n) (hG : (g : G), n g = 0) :
theorem add_monoid.exponent_min {G : Type u} [add_monoid G] (m : ) (hpos : 0 < m) (hm : m < ) :
(g : G), m g 0
theorem monoid.exponent_min {G : Type u} [monoid G] (m : ) (hpos : 0 < m) (hm : m < ) :
(g : G), g ^ m 1
@[simp]
theorem monoid.order_dvd_exponent {G : Type u} [monoid G] (g : G) :
theorem add_monoid.exponent_dvd_of_forall_nsmul_eq_zero (G : Type u_1) [add_monoid G] (n : ) (hG : (g : G), n g = 0) :
theorem monoid.exponent_dvd_of_forall_pow_eq_one (G : Type u_1) [monoid G] (n : ) (hG : (g : G), g ^ n = 1) :
theorem nat.prime.exists_order_of_eq_pow_factorization_exponent (G : Type u) [monoid G] {p : } (hp : nat.prime p) :
(g : G), = p ^ p
theorem monoid.exponent_ne_zero_iff_range_order_of_finite {G : Type u} [monoid G] (h : (g : G), 0 < ) :
theorem monoid.exponent_eq_zero_iff_range_order_of_infinite {G : Type u} [monoid G] (h : (g : G), 0 < ) :
theorem add_monoid.exponent_eq_supr_order_of {G : Type u} (h : (g : G), ) :
= (g : G),
theorem monoid.exponent_eq_supr_order_of {G : Type u} [comm_monoid G] (h : (g : G), 0 < ) :
= (g : G),
theorem add_monoid.exponent_eq_supr_order_of' {G : Type u}  :
= ite ( (g : G), = 0) 0 ( (g : G),
theorem monoid.exponent_eq_supr_order_of' {G : Type u} [comm_monoid G] :
= ite ( (g : G), = 0) 0 ( (g : G), order_of g)
theorem card_dvd_exponent_nsmul_rank' (G : Type u) [add_group.fg G] {n : } (hG : (g : G), n g = 0) :
theorem card_dvd_exponent_pow_rank' (G : Type u) [comm_group G] [group.fg G] {n : } (hG : (g : G), g ^ n = 1) :
n ^