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.

def AddMonoid.ExponentExists (G : Type u) [AddMonoid 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

• AddMonoid.ExponentExists G = ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), n • g = 0

def Monoid.ExponentExists (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

• Monoid.ExponentExists G = ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1

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

• AddMonoid.exponent G = if h : AddMonoid.ExponentExists G then Nat.find h else 0

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

• Monoid.exponent G = if h : Monoid.ExponentExists G then Nat.find h else 0

@[simp]

theorem AddMonoid.exponent_additive {G : Type u} [Monoid G] : AddMonoid.exponent (Additive G) = Monoid.exponent G

@[simp]

theorem Monoid.exponent_multiplicative {G : Type u_1} [AddMonoid G] : Monoid.exponent (Multiplicative G) = AddMonoid.exponent G

@[simp]

theorem AddOpposite.exponent {G : Type u} [AddMonoid G] : AddMonoid.exponent Gᵃᵒᵖ = AddMonoid.exponent G

@[simp]

theorem MulOpposite.exponent {G : Type u} [Monoid G] : Monoid.exponent Gᵐᵒᵖ = Monoid.exponent G

theorem AddMonoid.exponentExists_iff_ne_zero {G : Type u} [AddMonoid G] : AddMonoid.ExponentExists G ↔ AddMonoid.exponent G ≠ 0

theorem Monoid.exponentExists_iff_ne_zero {G : Type u} [Monoid G] : Monoid.ExponentExists G ↔ Monoid.exponent G ≠ 0

theorem AddMonoid.exponent_eq_zero_iff {G : Type u} [AddMonoid G] : AddMonoid.exponent G = 0 ↔ ¬AddMonoid.ExponentExists G

theorem Monoid.exponent_eq_zero_iff {G : Type u} [Monoid G] : Monoid.exponent G = 0 ↔ ¬Monoid.ExponentExists G

theorem AddMonoid.exponent_eq_zero_addOrder_zero {G : Type u} [AddMonoid G] {g : G} (hg : addOrderOf g = 0) : AddMonoid.exponent G = 0

abbrev AddMonoid.exponent_eq_zero_addOrder_zero.match_1 {G : Type u_1} [AddMonoid G] (motive : AddMonoid.ExponentExists G → Prop) : ∀ (x : AddMonoid.ExponentExists G), (∀ (n : ℕ) (hn : 0 < n) (hgn : ∀ (g : G), n • g = 0), motive (_ : ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), n • g = 0)) → motive x

Equations

• (_ : motive x) = (_ : motive x)

theorem Monoid.exponent_eq_zero_of_order_zero {G : Type u} [Monoid G] {g : G} (hg : orderOf g = 0) : Monoid.exponent G = 0

theorem AddMonoid.exponent_nsmul_eq_zero {G : Type u} [AddMonoid G] (g : G) : AddMonoid.exponent G • g = 0

theorem Monoid.pow_exponent_eq_one {G : Type u} [Monoid G] (g : G) : g ^ Monoid.exponent G = 1

theorem AddMonoid.nsmul_eq_mod_exponent {G : Type u} [AddMonoid G] {n : ℕ} (g : G) : n • g = (n % AddMonoid.exponent G) • g

theorem Monoid.pow_eq_mod_exponent {G : Type u} [Monoid G] {n : ℕ} (g : G) : g ^ n = g ^ (n % Monoid.exponent G)

theorem AddMonoid.exponent_pos_of_exists {G : Type u} [AddMonoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), n • g = 0) : 0 < AddMonoid.exponent G

theorem Monoid.exponent_pos_of_exists {G : Type u} [Monoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) : 0 < Monoid.exponent G

theorem AddMonoid.exponent_min' {G : Type u} [AddMonoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), n • g = 0) : AddMonoid.exponent G ≤ n

theorem Monoid.exponent_min' {G : Type u} [Monoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), g ^ n = 1) : Monoid.exponent G ≤ n

theorem AddMonoid.exponent_min {G : Type u} [AddMonoid G] (m : ℕ) (hpos : 0 < m) (hm : m < AddMonoid.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 AddMonoid.exp_eq_zero_of_subsingleton {G : Type u} [AddMonoid G] [Subsingleton G] : AddMonoid.exponent G = 1

@[simp]

theorem Monoid.exp_eq_one_of_subsingleton {G : Type u} [Monoid G] [Subsingleton G] : Monoid.exponent G = 1

theorem AddMonoid.addOrder_dvd_exponent {G : Type u} [AddMonoid G] (g : G) : addOrderOf g ∣ AddMonoid.exponent G

theorem Monoid.order_dvd_exponent {G : Type u} [Monoid G] (g : G) : orderOf g ∣ Monoid.exponent G

theorem AddMonoid.exponent_dvd_of_forall_nsmul_eq_zero (G : Type u_1) [AddMonoid G] (n : ℕ) (hG : ∀ (g : G), n • g = 0) : AddMonoid.exponent G ∣ n

theorem Monoid.exponent_dvd_of_forall_pow_eq_one (G : Type u_1) [Monoid G] (n : ℕ) (hG : ∀ (g : G), g ^ n = 1) : Monoid.exponent G ∣ n

theorem AddMonoid.lcm_addOrderOf_dvd_exponent (G : Type u) [AddMonoid G] [Fintype G] : Finset.lcm Finset.univ addOrderOf ∣ AddMonoid.exponent G

theorem Monoid.lcm_orderOf_dvd_exponent (G : Type u) [Monoid G] [Fintype G] : Finset.lcm Finset.univ orderOf ∣ Monoid.exponent G

theorem Nat.Prime.exists_addOrderOf_eq_pow_padic_val_nat_add_exponent (G : Type u) [AddMonoid G] {p : ℕ} (hp : Nat.Prime p) : ∃ (g : G), addOrderOf g = p ^ (Nat.factorization (AddMonoid.exponent G)) p

theorem Nat.Prime.exists_orderOf_eq_pow_factorization_exponent (G : Type u) [Monoid G] {p : ℕ} (hp : Nat.Prime p) : ∃ (g : G), orderOf g = p ^ (Nat.factorization (Monoid.exponent G)) p

theorem AddMonoid.exponent_eq_prime_iff {G : Type u_1} [AddMonoid G] [Nontrivial G] {p : ℕ} (hp : Nat.Prime p) : AddMonoid.exponent G = p ↔ ∀ (g : G), g ≠ 0 → addOrderOf g = p

theorem Monoid.exponent_eq_prime_iff {G : Type u_1} [Monoid G] [Nontrivial G] {p : ℕ} (hp : Nat.Prime p) : Monoid.exponent G = p ↔ ∀ (g : G), g ≠ 1 → orderOf g = 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} [AddMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) : AddMonoid.exponent G ≠ 0 ↔ Set.Finite (Set.range addOrderOf)

theorem Monoid.exponent_ne_zero_iff_range_orderOf_finite {G : Type u} [Monoid G] (h : ∀ (g : G), 0 < orderOf g) : Monoid.exponent G ≠ 0 ↔ Set.Finite (Set.range orderOf)

theorem AddMonoid.exponent_eq_zero_iff_range_addOrderOf_infinite {G : Type u} [AddMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) : AddMonoid.exponent G = 0 ↔ Set.Infinite (Set.range addOrderOf)

theorem Monoid.exponent_eq_zero_iff_range_orderOf_infinite {G : Type u} [Monoid G] (h : ∀ (g : G), 0 < orderOf g) : Monoid.exponent G = 0 ↔ Set.Infinite (Set.range orderOf)

theorem AddMonoid.lcm_addOrder_eq_exponent {G : Type u} [AddMonoid G] [Fintype G] : Finset.lcm Finset.univ addOrderOf = AddMonoid.exponent G

theorem Monoid.lcm_order_eq_exponent {G : Type u} [Monoid G] [Fintype G] : Finset.lcm Finset.univ orderOf = Monoid.exponent G

theorem AddMonoid.exponent_ne_zero_of_finite {G : Type u} [AddLeftCancelMonoid G] [Finite G] : AddMonoid.exponent G ≠ 0

theorem Monoid.exponent_ne_zero_of_finite {G : Type u} [LeftCancelMonoid G] [Finite G] : Monoid.exponent G ≠ 0

theorem AddMonoid.exponent_eq_iSup_addOrderOf {G : Type u} [AddCommMonoid G] (h : ∀ (g : G), 0 < addOrderOf g) : AddMonoid.exponent G = ⨆ (g : G), addOrderOf g

theorem Monoid.exponent_eq_iSup_orderOf {G : Type u} [CommMonoid G] (h : ∀ (g : G), 0 < orderOf g) : Monoid.exponent G = ⨆ (g : G), orderOf g

theorem AddMonoid.exponent_eq_iSup_addOrderOf' {G : Type u} [AddCommMonoid G] : AddMonoid.exponent G = if ∃ (g : G), addOrderOf g = 0 then 0 else ⨆ (g : G), addOrderOf g

theorem Monoid.exponent_eq_iSup_orderOf' {G : Type u} [CommMonoid G] : Monoid.exponent G = if ∃ (g : G), orderOf g = 0 then 0 else ⨆ (g : G), orderOf g

theorem AddMonoid.exponent_eq_max'_addOrderOf {G : Type u} [AddCancelCommMonoid G] [Fintype G] : AddMonoid.exponent G = Finset.max' (Finset.image addOrderOf Finset.univ) (_ : ∃ (x : ℕ), x ∈ Finset.image addOrderOf Finset.univ)

theorem Monoid.exponent_eq_max'_orderOf {G : Type u} [CancelCommMonoid G] [Fintype G] : Monoid.exponent G = Finset.max' (Finset.image orderOf Finset.univ) (_ : ∃ (x : ℕ), x ∈ Finset.image orderOf Finset.univ)

theorem AddGroup.one_lt_exponent {G : Type u} [AddGroup G] [Finite G] [Nontrivial G] : 1 < AddMonoid.exponent G

theorem Group.one_lt_exponent {G : Type u} [Group G] [Finite G] [Nontrivial G] : 1 < Monoid.exponent G

theorem card_dvd_exponent_nsmul_rank (G : Type u) [AddCommGroup G] [AddGroup.FG G] : Nat.card G ∣ AddMonoid.exponent G ^ AddGroup.rank G

theorem card_dvd_exponent_pow_rank (G : Type u) [CommGroup G] [Group.FG G] : Nat.card G ∣ Monoid.exponent G ^ Group.rank G

theorem card_dvd_exponent_nsmul_rank' (G : Type u) [AddCommGroup G] [AddGroup.FG G] {n : ℕ} (hG : ∀ (g : G), n • g = 0) : Nat.card G ∣ n ^ AddGroup.rank G

theorem card_dvd_exponent_pow_rank' (G : Type u) [CommGroup G] [Group.FG G] {n : ℕ} (hG : ∀ (g : G), g ^ n = 1) : Nat.card G ∣ n ^ Group.rank G

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} [AddMonoid M₁] [AddMonoid M₂] [FunLike F M₁ M₂] [AddMonoidHomClass F M₁ M₂] {f : F} (hf : Function.Surjective ⇑f) : AddMonoid.exponent M₂ ∣ AddMonoid.exponent M₁

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 : Function.Surjective ⇑f) : Monoid.exponent M₂ ∣ Monoid.exponent M₁

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

theorem AddMonoid.exponent_pi {ι : Type u_1} [Fintype ι] {M : ι → Type u_2} [(i : ι) → AddMonoid (M i)] : AddMonoid.exponent ((i : ι) → M i) = Finset.lcm Finset.univ 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} [Fintype ι] {M : ι → Type u_2} [(i : ι) → Monoid (M i)] : Monoid.exponent ((i : ι) → M i) = Finset.lcm Finset.univ 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 M₁] [AddMonoid M₂] : AddMonoid.exponent (M₁ × M₂) = lcm (AddMonoid.exponent M₁) (AddMonoid.exponent M₂)

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 (Monoid.exponent M₁) (Monoid.exponent M₂)

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