# 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).
• Monoid.exponent_pi and Monoid.exponent_prod: The exponent of a finite product of monoids is the least common multiple (Finset.lcm and lcm, respectively) of the exponents of the constituent monoids.
• MonoidHom.exponent_dvd: If f : M₁ →⋆ M₂ is surjective, then the exponent of M₂ divides the exponent of M₁.

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

Equations
Instances For

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

Equations
• = if h : then else 0
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.

Equations
• = if h : then else 0
Instances For
@[simp]
@[simp]
theorem Monoid.exponent_multiplicative {G : Type u_1} [] :
@[simp]
theorem AddOpposite.exponent {G : Type u} [] :
@[simp]
theorem MulOpposite.exponent {G : Type u} [] :
theorem AddMonoid.ExponentExists.isOfFinAddOrder {G : Type u} [] (h : ) {g : G} :
theorem Monoid.ExponentExists.isOfFinOrder {G : Type u} [] (h : ) {g : G} :
theorem AddMonoid.ExponentExists.addOrderOf_pos {G : Type u} [] (h : ) (g : G) :
0 <
theorem Monoid.ExponentExists.orderOf_pos {G : Type u} [] (h : ) (g : G) :
0 <
theorem Monoid.exponent_ne_zero {G : Type u} [] :

Alias of the reverse direction of Monoid.exponent_ne_zero.

@[deprecated]
@[deprecated]
theorem AddMonoid.exponent_pos {G : Type u} [] :
theorem Monoid.exponent_pos {G : Type u} [] :

Alias of the reverse direction of Monoid.exponent_pos.

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_eq_zero_iff_forall {G : Type u} [] :
n > 0, ∃ (g : G), n g 0

The exponent is zero iff for all nonzero n, one can find a g such that n • g ≠ 0.

theorem Monoid.exponent_eq_zero_iff_forall {G : Type u} [] :
n > 0, ∃ (g : G), g ^ n 1

The exponent is zero iff for all nonzero n, one can find a g such that g ^ n ≠ 1.

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 : G), m g 0
theorem Monoid.exponent_min {G : Type u} [] (m : ) (hpos : 0 < m) (hm : ) :
∃ (g : G), g ^ m 1
theorem Monoid.exp_eq_one_iff {G : Type u} [] :
@[simp]
theorem AddMonoid.exp_eq_one_of_subsingleton {G : Type u} [] [hs : ] :
@[simp]
theorem Monoid.exp_eq_one_of_subsingleton {G : Type u} [] [hs : ] :
theorem Monoid.order_dvd_exponent {G : Type u} [] (g : G) :
theorem AddMonoid.addOrderOf_le_exponent {G : Type u} [] (h : ) (g : G) :
theorem Monoid.orderOf_le_exponent {G : Type u} [] (h : ) (g : G) :
theorem AddMonoid.exponent_dvd_iff_forall_nsmul_eq_zero {G : Type u} [] {n : } :
∀ (g : G), n g = 0
theorem Monoid.exponent_dvd_iff_forall_pow_eq_one {G : Type u} [] {n : } :
∀ (g : G), g ^ n = 1
theorem Monoid.exponent_dvd_of_forall_pow_eq_one {G : Type u} [] {n : } :
(∀ (g : G), g ^ n = 1)

Alias of the reverse direction of Monoid.exponent_dvd_iff_forall_pow_eq_one.

theorem AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero {G : Type u} [] {n : } :
(∀ (g : G), n g = 0)
theorem AddMonoid.exponent_dvd {G : Type u} [] {n : } :
∀ (g : G), n
theorem Monoid.exponent_dvd {G : Type u} [] {n : } :
∀ (g : G), n
@[deprecated]
theorem AddMonoid.exponent_dvd_of_forall_addOrderOf_dvd (G : Type u) [] (n : ) (h : ∀ (g : G), n) :
@[deprecated]
theorem Monoid.exponent_dvd_of_forall_orderOf_dvd (G : Type u) [] (n : ) (h : ∀ (g : G), n) :
theorem Monoid.lcm_orderOf_dvd_exponent (G : Type u) [] [] :
Finset.univ.lcm orderOf
∃ (g : G), = p ^ .factorization p
theorem Nat.Prime.exists_orderOf_eq_pow_factorization_exponent (G : Type u) [] {p : } (hp : ) :
∃ (g : G), = p ^ ().factorization p
theorem AddCommute.addOrderOf_add_nsmul_eq_lcm {G : Type u} [] {x : G} {y : G} (h : ) (hx : 0) (hy : 0) :
addOrderOf (( / ().factorizationLCMLeft ()) x + ( / ().factorizationLCMRight ()) y) = ().lcm ()

If two commuting elements x and y of an additive monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the sum of a multiple of x and a multiple of y. See also the result below if you don't need the explicit formula.

theorem Commute.orderOf_mul_pow_eq_lcm {G : Type u} [] {x : G} {y : G} (h : Commute x y) (hx : 0) (hy : 0) :
orderOf (x ^ ( / ().factorizationLCMLeft ()) * y ^ ( / ().factorizationLCMRight ())) = ().lcm ()

If two commuting elements x and y of a monoid have order n and m, there is an element of order lcm n m. The result actually gives an explicit (computable) element, written as the product of a power of x and a power of y. See also the result below if you don't need the explicit formula.

theorem AddCommute.exists_addOrderOf_eq_lcm (G : Type u) [] {x : G} {y : G} (h : ) :
zAddSubmonoid.closure {x, y}, = ().lcm ()

If two commuting elements x and y of an additive monoid have order n and m, then there is an element of order lcm n m that lies in the additive subgroup generated by x and y.

theorem Commute.exists_orderOf_eq_lcm (G : Type u) [] {x : G} {y : G} (h : Commute x y) :
zSubmonoid.closure {x, y}, = ().lcm ()

If two commuting elements x and y of a monoid have order n and m, then there is an element of order lcm n m that lies in the subgroup generated by x and y.

theorem AddMonoid.exponent_eq_prime_iff {G : Type u_1} [] [] {p : } (hp : ) :
∀ (g : G), g 0 = p
theorem Monoid.exponent_eq_prime_iff {G : Type u_1} [] [] {p : } (hp : ) :
∀ (g : G), g 1 = p

A nontrivial monoid has prime exponent p if and only if every non-identity element has order 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 < ) :
(Set.range orderOf).Finite
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 < ) :
(Set.range orderOf).Infinite
theorem Monoid.lcm_orderOf_eq_exponent {G : Type u} [] [] :
Finset.univ.lcm orderOf =
@[deprecated]
theorem Monoid.lcm_order_eq_exponent {G : Type u} [] [] :
Finset.univ.lcm orderOf =

Alias of Monoid.lcm_orderOf_eq_exponent.

@[deprecated]
theorem AddMonoid.exponent_dvd_of_addMonoidHom {G : Type u} [] {H : Type u_1} [] (e : G →+ H) (e_inj : ) :

If there exists an injective, addition-preserving map from G to H, then the exponent of G divides the exponent of H.

theorem Monoid.exponent_dvd_of_monoidHom {G : Type u} [] {H : Type u_1} [] (e : G →* H) (e_inj : ) :

If there exists an injective, multiplication-preserving map from G to H, then the exponent of G divides the exponent of H.

theorem AddMonoid.exponent_eq_of_addEquiv {G : Type u} [] {H : Type u_1} [] (e : G ≃+ H) :

If there exists a addition-preserving equivalence between G and H, then the exponent of G is equal to the exponent of H.

theorem Monoid.exponent_eq_of_mulEquiv {G : Type u} [] {H : Type u_1} [] (e : G ≃* H) :

If there exists a multiplication-preserving equivalence between G and H, then the exponent of G is equal to the exponent of H.

@[simp]
theorem AddSubmonoid.exponent_top (G : Type u) [] :
@[simp]
theorem Submonoid.exponent_top (G : Type u) [] :
theorem AddSubmonoid.nsmul_exponent_eq_zero {G : Type u} [] {S : } {g : G} (g_in_s : g S) :
= 0
theorem Submonoid.pow_exponent_eq_one {G : Type u} [] {S : } {g : G} (g_in_s : g S) :
g ^ = 1
theorem AddMonoid.one_lt_exponent {G : Type u} [] [] :
theorem Monoid.one_lt_exponent {G : Type u} [] [] [] :
∃ (g : G),
theorem Monoid.exists_orderOf_eq_exponent {G : Type u} [] (hG : ) :
∃ (g : G),
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),
= if ∃ (g : G), = 0 then 0 else ⨆ (g : G),
theorem Monoid.exponent_eq_iSup_orderOf' {G : Type u} [] :
= if ∃ (g : G), = 0 then 0 else ⨆ (g : G),
theorem Monoid.exponent_eq_max'_orderOf {G : Type u} [] [] :
= (Finset.image orderOf Finset.univ).max'
@[deprecated Monoid.one_lt_exponent]
theorem AddGroup.one_lt_exponent {G : Type u} [] [] [] :
@[deprecated Monoid.one_lt_exponent]
theorem Group.one_lt_exponent {G : Type u} [] [] [] :
theorem Group.exponent_dvd_card {G : Type u} [] [] :
theorem Subgroup.exponent_toSubmonoid {G : Type u} [] (H : ) :
Monoid.exponent H.toSubmonoid =
@[simp]
theorem AddSubgroup.exponent_top {G : Type u} [] :
@[simp]
theorem Subgroup.exponent_top {G : Type u} [] :
theorem AddSubgroup.nsmul_exponent_eq_zero {G : Type u} [] {H : } {g : G} (g_in_H : g H) :
= 0
theorem Subgroup.pow_exponent_eq_one {G : Type u} [] {H : } {g : G} (g_in_H : g H) :
g ^ = 1
theorem AddMonoid.exponent_pi_eq_zero {ι : Type u_1} {M : ιType u_2} [(i : ι) → AddMonoid (M i)] {j : ι} (hj : AddMonoid.exponent (M j) = 0) :
AddMonoid.exponent ((i : ι) → M i) = 0
theorem Monoid.exponent_pi_eq_zero {ι : Type u_1} {M : ιType u_2} [(i : ι) → Monoid (M i)] {j : ι} (hj : Monoid.exponent (M j) = 0) :
Monoid.exponent ((i : ι) → M i) = 0
theorem AddMonoidHom.exponent_dvd {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [] [] [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {f : F} (hf : ) :
theorem MonoidHom.exponent_dvd {F : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [Monoid M₁] [Monoid M₂] [FunLike F M₁ M₂] [MonoidHomClass F M₁ M₂] {f : F} (hf : ) :

If f : M₁ →⋆ M₂ is surjective, then the exponent of M₂ divides the exponent of M₁.

theorem AddMonoid.exponent_pi {ι : Type u_1} [] {M : ιType u_2} [(i : ι) → AddMonoid (M i)] :
AddMonoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun (x : ι) => AddMonoid.exponent (M x)

The exponent of finite product of additive monoids is the Finset.lcm of the exponents of the constituent additive monoids.

theorem Monoid.exponent_pi {ι : Type u_1} [] {M : ιType u_2} [(i : ι) → Monoid (M i)] :
Monoid.exponent ((i : ι) → M i) = Finset.univ.lcm fun (x : ι) => Monoid.exponent (M x)

The exponent of finite product of monoids is the Finset.lcm of the exponents of the constituent monoids.

theorem AddMonoid.exponent_prod {M₁ : Type u_1} {M₂ : Type u_2} [] [] :
AddMonoid.exponent (M₁ × M₂) = lcm () ()

The exponent of product of two additive monoids is the lcm of the exponents of the individuaul additive monoids.

theorem Monoid.exponent_prod {M₁ : Type u_1} {M₂ : Type u_2} [Monoid M₁] [Monoid M₂] :
Monoid.exponent (M₁ × M₂) = lcm () ()

The exponent of product of two monoids is the lcm of the exponents of the individuaul monoids.

# Properties of monoids with exponent two #

theorem addOrderOf_eq_two_iff {G : Type u} [] (hG : ) {x : G} :
= 2 x 0
theorem orderOf_eq_two_iff {G : Type u} [] (hG : ) {x : G} :
= 2 x 1
theorem AddCommute.of_addOrderOf_dvd_two {G : Type u} [] [] (h : ∀ (g : G), 2) (a : G) (b : G) :
theorem Commute.of_orderOf_dvd_two {G : Type u} [] [] (h : ∀ (g : G), 2) (a : G) (b : G) :
theorem add_comm_of_exponent_two {G : Type u} [] [] (hG : ) (a : G) (b : G) :
a + b = b + a
theorem mul_comm_of_exponent_two {G : Type u} [] [] (hG : ) (a : G) (b : G) :
a * b = b * a

In a cancellative monoid of exponent two, all elements commute.

@[reducible]
def addCommMonoidOfExponentTwo {G : Type u} [] [] (hG : ) :

Any additive group of exponent two is abelian.

Equations
Instances For
@[reducible]
def commMonoidOfExponentTwo {G : Type u} [] [] (hG : ) :

Any cancellative monoid of exponent two is abelian.

Equations
Instances For
theorem neg_eq_self_of_exponent_two {G : Type u} [] (hG : ) (x : G) :
-x = x
theorem inv_eq_self_of_exponent_two {G : Type u} [] (hG : ) (x : G) :
x⁻¹ = x

In a group of exponent two, every element is its own inverse.

theorem neg_eq_self_of_addOrderOf_eq_two {G : Type u} [] {x : G} (hx : = 2) :
-x = x
theorem inv_eq_self_of_orderOf_eq_two {G : Type u} [] {x : G} (hx : = 2) :
x⁻¹ = x

If an element in a group has order two, then it is its own inverse.

theorem instAddCommGroupOfExponentTwo.proof_1 {G : Type u_1} [] (hG : ) (a : G) (b : G) :
a + b = b + a
@[reducible, deprecated]
def instAddCommGroupOfExponentTwo {G : Type u} [] (hG : ) :

Any additive group of exponent two is abelian.

Equations
Instances For
@[reducible, deprecated]
def instCommGroupOfExponentTwo {G : Type u} [] (hG : ) :

Any group of exponent two is abelian.

Equations
Instances For
theorem add_not_mem_of_addOrderOf_eq_two {G : Type u} [] {x : G} {y : G} (hx : = 2) (hy : = 2) (hxy : x y) :
x + y{x, y, 0}
theorem mul_not_mem_of_orderOf_eq_two {G : Type u} [] {x : G} {y : G} (hx : = 2) (hy : = 2) (hxy : x y) :
x * y{x, y, 1}
theorem add_not_mem_of_exponent_two {G : Type u} [] (h : ) {x : G} {y : G} (hx : x 0) (hy : y 0) (hxy : x y) :
x + y{x, y, 0}
theorem mul_not_mem_of_exponent_two {G : Type u} [] (h : ) {x : G} {y : G} (hx : x 1) (hy : y 1) (hxy : x y) :
x * y{x, y, 1}