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

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.

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.

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.

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.

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

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

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

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, m • g ≠ 0

theorem Monoid.exponent_min {G : Type u} [Monoid G] (m : ℕ) (hpos : 0 < m) (hm : m < Monoid.exponent 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, 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, orderOf g = p ^ ↑(Nat.factorization (Monoid.exponent G)) 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, 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, 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 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