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 #

monoid.exponent_exists 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.
add_monoid.exponent_exists the additive version of monoid.exponent_exists.
add_monoid.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_supr_order_of('): For a commutative cancel monoid, the exponent is equal to ⨆ g : G, order_of 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 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

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

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

monoid.exponent_exists G = ∃ (n : ℕ), 0 < n ∧ ∀ (g : G), g ^ n = 1

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 = dite (monoid.exponent_exists G) (λ (h : monoid.exponent_exists G), nat.find h) (λ (h : ¬monoid.exponent_exists G), 0)

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

add_monoid.exponent G = dite (add_monoid.exponent_exists G) (λ (h : add_monoid.exponent_exists G), nat.find h) (λ (h : ¬add_monoid.exponent_exists G), 0)

theorem add_monoid.exponent_exists_iff_ne_zero {G : Type u} [add_monoid G] :

add_monoid.exponent_exists G ↔ add_monoid.exponent G ≠ 0

theorem monoid.exponent_exists_iff_ne_zero {G : Type u} [monoid G] :

monoid.exponent_exists G ↔ monoid.exponent G ≠ 0

theorem add_monoid.exponent_eq_zero_iff {G : Type u} [add_monoid G] :

add_monoid.exponent G = 0 ↔ ¬add_monoid.exponent_exists G

theorem monoid.exponent_eq_zero_iff {G : Type u} [monoid G] :

monoid.exponent G = 0 ↔ ¬monoid.exponent_exists G

theorem add_monoid.exponent_eq_zero_of_order_zero {G : Type u} [add_monoid G] {g : G} (hg : add_order_of g = 0) :

add_monoid.exponent G = 0

theorem monoid.exponent_eq_zero_of_order_zero {G : Type u} [monoid G] {g : G} (hg : order_of g = 0) :

monoid.exponent G = 0

theorem monoid.pow_exponent_eq_one {G : Type u} [monoid G] (g : G) :

g ^ monoid.exponent G = 1

theorem add_monoid.exponent_nsmul_eq_zero {G : Type u} [add_monoid G] (g : G) :

add_monoid.exponent G • g = 0

theorem add_monoid.nsmul_eq_mod_exponent {G : Type u} [add_monoid G] {n : ℕ} (g : G) :

n • g = (n % add_monoid.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 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 add_monoid.exponent_pos_of_exists {G : Type u} [add_monoid G] (n : ℕ) (hpos : 0 < n) (hG : ∀ (g : G), n • g = 0) :

0 < add_monoid.exponent G

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

monoid.exponent G ≤ n

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

add_monoid.exponent G ≤ n

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 add_monoid.exp_eq_zero_of_subsingleton {G : Type u} [add_monoid G] [subsingleton G] :

add_monoid.exponent G = 1

@[simp]

theorem monoid.exp_eq_one_of_subsingleton {G : Type u} [monoid G] [subsingleton G] :

monoid.exponent G = 1

theorem add_monoid.add_order_dvd_exponent {G : Type u} [add_monoid G] (g : G) :

add_order_of g ∣ add_monoid.exponent G

theorem monoid.order_dvd_exponent {G : Type u} [monoid G] (g : G) :

order_of g ∣ monoid.exponent 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) :

add_monoid.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 add_monoid.lcm_add_order_of_dvd_exponent (G : Type u) [add_monoid G] [fintype G] :

finset.univ.lcm add_order_of ∣ add_monoid.exponent G

theorem monoid.lcm_order_of_dvd_exponent (G : Type u) [monoid G] [fintype G] :

finset.univ.lcm order_of ∣ monoid.exponent G

theorem nat.prime.exists_order_of_eq_pow_padic_val_nat_add_exponent (G : Type u) [add_monoid G] {p : ℕ} (hp : nat.prime p) :

∃ (g : G), add_order_of g = p ^ ⇑((add_monoid.exponent G).factorization) p

theorem nat.prime.exists_order_of_eq_pow_factorization_exponent (G : Type u) [monoid G] {p : ℕ} (hp : nat.prime p) :

∃ (g : G), order_of g = p ^ ⇑((monoid.exponent G).factorization) p

theorem monoid.exponent_ne_zero_iff_range_order_of_finite {G : Type u} [monoid G] (h : ∀ (g : G), 0 < order_of g) :

monoid.exponent G ≠ 0 ↔ (set.range order_of).finite

theorem add_monoid.exponent_ne_zero_iff_range_order_of_finite {G : Type u} [add_monoid G] (h : ∀ (g : G), 0 < add_order_of g) :

add_monoid.exponent G ≠ 0 ↔ (set.range add_order_of).finite

theorem monoid.exponent_eq_zero_iff_range_order_of_infinite {G : Type u} [monoid G] (h : ∀ (g : G), 0 < order_of g) :

monoid.exponent G = 0 ↔ (set.range order_of).infinite

theorem add_monoid.exponent_eq_zero_iff_range_order_of_infinite {G : Type u} [add_monoid G] (h : ∀ (g : G), 0 < add_order_of g) :

add_monoid.exponent G = 0 ↔ (set.range add_order_of).infinite

theorem monoid.lcm_order_eq_exponent {G : Type u} [monoid G] [fintype G] :

finset.univ.lcm order_of = monoid.exponent G

theorem add_monoid.lcm_add_order_eq_exponent {G : Type u} [add_monoid G] [fintype G] :

finset.univ.lcm add_order_of = add_monoid.exponent G

theorem monoid.exponent_ne_zero_of_finite {G : Type u} [left_cancel_monoid G] [finite G] :

monoid.exponent G ≠ 0

theorem add_monoid.exponent_ne_zero_of_finite {G : Type u} [add_left_cancel_monoid G] [finite G] :

add_monoid.exponent G ≠ 0

theorem add_monoid.exponent_eq_supr_order_of {G : Type u} [add_comm_monoid G] (h : ∀ (g : G), 0 < add_order_of g) :

add_monoid.exponent G = ⨆ (g : G), add_order_of g

theorem monoid.exponent_eq_supr_order_of {G : Type u} [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_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} [comm_monoid G] :

monoid.exponent G = ite (∃ (g : G), order_of g = 0) 0 (⨆ (g : G), order_of g)

theorem add_monoid.exponent_eq_max'_order_of {G : Type u} [add_cancel_comm_monoid G] [fintype G] :

add_monoid.exponent G = (finset.image add_order_of finset.univ).max' _

theorem monoid.exponent_eq_max'_order_of {G : Type u} [cancel_comm_monoid G] [fintype G] :

monoid.exponent G = (finset.image order_of finset.univ).max' _

theorem card_dvd_exponent_pow_rank (G : Type u) [comm_group G] [group.fg G] :

nat.card G ∣ monoid.exponent G ^ group.rank G

theorem card_dvd_exponent_nsmul_rank (G : Type u) [add_comm_group G] [add_group.fg G] :

nat.card G ∣ add_monoid.exponent G ^ add_group.rank 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) :

nat.card G ∣ n ^ add_group.rank G

theorem card_dvd_exponent_pow_rank' (G : Type u) [comm_group G] [group.fg G] {n : ℕ} (hG : ∀ (g : G), g ^ n = 1) :

nat.card G ∣ n ^ group.rank G