mathlibdocumentation

group_theory.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.

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
• = ∃ (n : ), 0 < n ∀ (g : G), g ^ n = 1
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 monoid.exponent_eq_zero_iff {G : Type u} [monoid G] :
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]
@[simp]
theorem monoid.exp_eq_one_of_subsingleton {G : Type u} [monoid G] [subsingleton G] :
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 monoid.lcm_order_of_dvd_exponent (G : Type u) [monoid G] [fintype G] :
∃ (g : G), =
theorem nat.prime.exists_order_of_eq_pow_padic_val_nat_exponent (G : Type u) [monoid G] {p : } (hp : nat.prime p) :
∃ (g : G), = p ^
theorem monoid.exponent_ne_zero_iff_range_order_of_finite {G : Type u} [monoid G] (h : ∀ (g : G), 0 < ) :
theorem add_monoid.exponent_ne_zero_iff_range_order_of_finite {G : Type u} [add_monoid G] (h : ∀ (g : G), ) :
theorem monoid.exponent_eq_zero_iff_range_order_of_infinite {G : Type u} [monoid G] (h : ∀ (g : G), 0 < ) :
theorem add_monoid.exponent_eq_zero_iff_range_order_of_infinite {G : Type u} [add_monoid G] (h : ∀ (g : G), ) :
theorem monoid.lcm_order_eq_exponent {G : Type u} [fintype G] :
theorem monoid.exponent_ne_zero_of_fintype {G : Type u} [fintype G] :
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} (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}  :
= ite (∃ (g : G), = 0) 0 (⨆ (g : G), order_of g)
theorem monoid.exponent_eq_max'_order_of {G : Type u} [fintype G] :