mathlib documentation

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.

Main definitions #

Main results #

TODO #

def add_monoid.exponent_exists (G : Type u) [add_monoid G] :
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
noncomputable def add_monoid.exponent (G : Type u) [add_monoid G] :

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_of_order_zero {G : Type u} [monoid G] {g : G} (hg : order_of g = 0) :
theorem monoid.pow_exponent_eq_one {G : Type u} [monoid G] (g : G) :
theorem add_monoid.exponent_nsmul_eq_zero {G : Type u} [add_monoid G] (g : G) :
theorem add_monoid.nsmul_eq_mod_exponent {G : Type u} [add_monoid G] {n : } (g : G) :
theorem monoid.pow_eq_mod_exponent {G : Type u} [monoid G] {n : } (g : G) :
g ^ n = g ^ (n % monoid.exponent G)
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 < add_monoid.exponent G) :
∃ (g : G), m g 0
theorem monoid.exponent_min {G : Type u} [monoid G] (m : ) (hpos : 0 < m) (hm : m < monoid.exponent G) :
∃ (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 add_monoid.exponent_eq_supr_order_of {G : Type u} [add_cancel_comm_monoid G] (h : ∀ (g : G), 0 < add_order_of g) :
theorem monoid.exponent_eq_supr_order_of {G : Type u} [cancel_comm_monoid G] (h : ∀ (g : G), 0 < order_of g) :
monoid.exponent G = ⨆ (g : G), order_of g
theorem add_monoid.exponent_eq_supr_order_of' {G : Type u} [add_cancel_comm_monoid G] :
add_monoid.exponent G = ite (∃ (g : G), add_order_of g = 0) 0 (⨆ (g : G), add_order_of g)
theorem monoid.exponent_eq_supr_order_of' {G : Type u} [cancel_comm_monoid G] :
monoid.exponent G = ite (∃ (g : G), order_of g = 0) 0 (⨆ (g : G), order_of g)