mathlib3 documentation

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 #

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.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
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.exponent_eq_supr_order_of {G : Type u} [comm_monoid G] (h : (g : G), 0 < order_of g) :
theorem monoid.exponent_eq_supr_order_of' {G : Type u} [comm_monoid G] :
monoid.exponent G = ite ( (g : G), order_of g = 0) 0 ( (g : G), order_of g)
theorem card_dvd_exponent_nsmul_rank' (G : Type u) [add_comm_group G] [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) :