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.exponent_exists
is a predicate on a monoidG
saying that there is some positiven
such thatg ^ n = 1
for allg ∈ G
.monoid.exponent
defines the exponent of a monoidG
as the minimal positiven
such thatg ^ n = 1
for allg ∈ G
, by convention it is0
if no suchn
exists.add_monoid.exponent_exists
the additive version ofmonoid.exponent_exists
.add_monoid.exponent
the additive version ofmonoid.exponent
.
Main results #
monoid.lcm_order_eq_exponent
: For a finite left cancel monoidG
, the exponent is equal to thefinset.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.
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)
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_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
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
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
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) :
@[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.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
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
add_monoid.exponent_ne_zero_iff_range_order_of_finite
{G : Type u}
[add_monoid G]
(h : ∀ (g : G), 0 < add_order_of g) :
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) :
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
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]
{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