mathlib documentation

group_theory.order_of_element

Order of an element #

This file defines the order of an element of a finite group. For a finite group G the order of x ∈ G is the minimal n ≥ 1 such that x ^ n = 1.

Main definitions #

Tags #

order of an element

source
theorem is_periodic_pt_add_iff_nsmul_eq_zero {A : Type v} {n : ℕ} [add_monoid A] (a : A) :
function.is_periodic_pt (has_add.add a) n 0 ↔ n • a = 0
source
theorem is_periodic_pt_mul_iff_pow_eq_one {G : Type u} {n : ℕ} [monoid G] (x : G) :
function.is_periodic_pt (has_mul.mul x) n 1 ↔ x ^ n = 1
source
def is_of_fin_add_order {A : Type v} [add_monoid A] (a : A) :
Prop

is_of_fin_add_order is a predicate on an element a of an additive monoid to be of finite order, i.e. there exists n ≥ 1 such that n • a = 0.

Equations
source
def is_of_fin_order {G : Type u} [monoid G] (x : G) :
Prop

is_of_fin_order is a predicate on an element x of a monoid to be of finite order, i.e. there exists n ≥ 1 such that x ^ n = 1.

Equations
source
theorem is_of_fin_add_order_of_mul_iff {G : Type u} {x : G} [monoid G] :
is_of_fin_add_order (⇑additive.of_mul x) ↔ is_of_fin_order x
source
theorem is_of_fin_order_of_add_iff {A : Type v} {a : A} [add_monoid A] :
is_of_fin_order (⇑multiplicative.of_add a) ↔ is_of_fin_add_order a
source
theorem is_of_fin_add_order_iff_nsmul_eq_zero {A : Type v} [add_monoid A] (a : A) :
is_of_fin_add_order a ↔ ∃ (n : ℕ), 0 < n ∧ n • a = 0
source
theorem is_of_fin_order_iff_pow_eq_one {G : Type u} [monoid G] (x : G) :
is_of_fin_order x ↔ ∃ (n : ℕ), 0 < n ∧ x ^ n = 1
source
def add_order_of {A : Type v} [add_monoid A] (a : A) :
ℕ

add_order_of a is the order of the element a, i.e. the n ≥ 1, s.t. n • a = 0 if it exists. Otherwise, i.e. if a is of infinite order, then add_order_of a is 0 by convention.

Equations
source
def order_of {G : Type u} [monoid G] (x : G) :
ℕ

order_of x is the order of the element x, i.e. the n ≥ 1, s.t. x ^ n = 1 if it exists. Otherwise, i.e. if x is of infinite order, then order_of x is 0 by convention.

Equations
source
theorem commute.order_of_mul_dvd_lcm {G : Type u} {x y : G} [monoid G] (h : commute x y) :
order_of (x * y) ∣ (order_of x).lcm (order_of y)
source
theorem add_commute.order_of_add_dvd_lcm {G : Type u} {x y : G} [add_monoid G] (h : add_commute x y) :
add_order_of (x + y) ∣ (add_order_of x).lcm (add_order_of y)
source
@[simp]
theorem add_order_of_of_mul_eq_order_of {G : Type u} [monoid G] (x : G) :
add_order_of (⇑additive.of_mul x) = order_of x
source
@[simp]
theorem order_of_of_add_eq_add_order_of {A : Type v} [add_monoid A] (a : A) :
order_of (⇑multiplicative.of_add a) = add_order_of a
source
theorem add_order_of_pos' {G : Type u} {x : G} [add_monoid G] (h : is_of_fin_add_order x) :
0 < add_order_of x
source
theorem order_of_pos' {G : Type u} {x : G} [monoid G] (h : is_of_fin_order x) :
0 < order_of x
source
theorem pow_order_of_eq_one {G : Type u} [monoid G] (x : G) :
x ^ order_of x = 1
source
theorem add_order_of_nsmul_eq_zero {A : Type v} [add_monoid A] (a : A) :
add_order_of a • a = 0
source
theorem order_of_eq_zero {G : Type u} {x : G} [monoid G] (h : ¬is_of_fin_order x) :
order_of x = 0
source
theorem add_order_of_eq_zero {G : Type u} {x : G} [add_monoid G] (h : ¬is_of_fin_add_order x) :
add_order_of x = 0
source
theorem add_order_of_eq_zero_iff {G : Type u} {x : G} [add_monoid G] :
add_order_of x = 0 ↔ ¬is_of_fin_add_order x
source
theorem order_of_eq_zero_iff {G : Type u} {x : G} [monoid G] :
order_of x = 0 ↔ ¬is_of_fin_order x
source
theorem nsmul_ne_zero_of_lt_add_order_of' {A : Type v} {a : A} {n : ℕ} [add_monoid A] (n0 : n ≠ 0) (h : n < add_order_of a) :
n • a ≠ 0
source
theorem pow_eq_one_of_lt_order_of' {G : Type u} {x : G} {n : ℕ} [monoid G] (n0 : n ≠ 0) (h : n < order_of x) :
x ^ n ≠ 1
source
theorem add_order_of_le_of_nsmul_eq_zero {A : Type v} {a : A} {n : ℕ} [add_monoid A] (hn : 0 < n) (h : n • a = 0) :
add_order_of a ≤ n
source
theorem order_of_le_of_pow_eq_one {G : Type u} {x : G} {n : ℕ} [monoid G] (hn : 0 < n) (h : x ^ n = 1) :
order_of x ≤ n
source
@[simp]
theorem order_of_one {G : Type u} [monoid G] :
order_of 1 = 1
source
@[simp]
theorem add_order_of_zero {A : Type v} [add_monoid A] :
add_order_of 0 = 1
source
@[simp]
theorem order_of_eq_one_iff {G : Type u} {x : G} [monoid G] :
order_of x = 1 ↔ x = 1
source
@[simp]
theorem add_order_of_eq_one_iff {A : Type v} {a : A} [add_monoid A] :
add_order_of a = 1 ↔ a = 0
source
theorem pow_eq_mod_order_of {G : Type u} {x : G} [monoid G] {n : ℕ} :
x ^ n = x ^ (n % order_of x)
source
theorem nsmul_eq_mod_add_order_of {A : Type v} {a : A} [add_monoid A] {n : ℕ} :
n • a = (n % add_order_of a) • a
source
theorem order_of_dvd_of_pow_eq_one {G : Type u} {x : G} {n : ℕ} [monoid G] (h : x ^ n = 1) :
order_of x ∣ n
source
theorem add_order_of_dvd_of_nsmul_eq_zero {A : Type v} {a : A} {n : ℕ} [add_monoid A] (h : n • a = 0) :
add_order_of a ∣ n
source
theorem add_order_of_dvd_iff_nsmul_eq_zero {A : Type v} {a : A} [add_monoid A] {n : ℕ} :
add_order_of a ∣ n ↔ n • a = 0
source
theorem order_of_dvd_iff_pow_eq_one {G : Type u} {x : G} [monoid G] {n : ℕ} :
order_of x ∣ n ↔ x ^ n = 1
source
theorem exists_pow_eq_self_of_coprime {G : Type u} {x : G} {n : ℕ} [monoid G] (h : n.coprime (order_of x)) :
∃ (m : ℕ), (x ^ n) ^ m = x
source
theorem exists_nsmul_eq_self_of_coprime {A : Type v} {n : ℕ} [add_monoid A] (a : A) (h : n.coprime (add_order_of a)) :
∃ (m : ℕ), m • n • a = a
source
theorem add_order_of_eq_add_order_of_iff {A : Type v} {a : A} [add_monoid A] {B : Type u_1} [add_monoid B] {b : B} :
add_order_of a = add_order_of b ↔ ∀ (n : ℕ), n • a = 0 ↔ n • b = 0
source
theorem order_of_eq_order_of_iff {G : Type u} {x : G} [monoid G] {H : Type u_1} [monoid H] {y : H} :
order_of x = order_of y ↔ ∀ (n : ℕ), x ^ n = 1 ↔ y ^ n = 1
source
theorem add_order_of_injective {A : Type v} [add_monoid A] {B : Type u_1} [add_monoid B] (f : A →+ B) (hf : function.injective ⇑f) (a : A) :
add_order_of (⇑f a) = add_order_of a
source
theorem order_of_injective {G : Type u} [monoid G] {H : Type u_1} [monoid H] (f : G →* H) (hf : function.injective ⇑f) (x : G) :
order_of (⇑f x) = order_of x
source
@[simp]
theorem order_of_submonoid {G : Type u} [monoid G] {H : submonoid G} (y : ↥H) :
order_of ↑y = order_of y
source
@[simp]
theorem order_of_add_submonoid {G : Type u} [add_monoid G] {H : add_submonoid G} (y : ↥H) :
add_order_of ↑y = add_order_of y
source
theorem order_of_pow' {G : Type u} (x : G) {n : ℕ} [monoid G] (h : n ≠ 0) :
order_of (x ^ n) = order_of x / (order_of x).gcd n
source
theorem add_order_of_nsmul' {A : Type v} (a : A) {n : ℕ} [add_monoid A] (h : n ≠ 0) :
add_order_of (n • a) = add_order_of a / (add_order_of a).gcd n
source
theorem order_of_pow'' {G : Type u} (x : G) (n : ℕ) [monoid G] (h : is_of_fin_order x) :
order_of (x ^ n) = order_of x / (order_of x).gcd n
source
theorem add_order_of_nsmul'' {A : Type v} (a : A) (n : ℕ) [add_monoid A] (h : is_of_fin_add_order a) :
add_order_of (n • a) = add_order_of a / (add_order_of a).gcd n
source
theorem add_order_of_eq_prime {A : Type v} {a : A} [add_monoid A] {p : ℕ} [hp : fact (nat.prime p)] (hg : p • a = 0) (hg1 : a ≠ 0) :
add_order_of a = p
source
theorem order_of_eq_prime {G : Type u} {x : G} [monoid G] {p : ℕ} [hp : fact (nat.prime p)] (hg : x ^ p = 1) (hg1 : x ≠ 1) :
order_of x = p
source
theorem add_order_of_eq_prime_pow {A : Type v} {a : A} {n : ℕ} [add_monoid A] {p : ℕ} [hp : fact (nat.prime p)] (hnot : ¬p ^ n • a = 0) (hfin : p ^ (n + 1) • a = 0) :
add_order_of a = p ^ (n + 1)
source
theorem order_of_eq_prime_pow {G : Type u} {x : G} {n : ℕ} [monoid G] {p : ℕ} [hp : fact (nat.prime p)] (hnot : ¬x ^ p ^ n = 1) (hfin : x ^ p ^ (n + 1) = 1) :
order_of x = p ^ (n + 1)
source
theorem pow_injective_aux {G : Type u} (x : G) {n m : ℕ} [left_cancel_monoid G] (h : n ≤ m) (hm : m < order_of x) (eq : x ^ n = x ^ m) :
n = m
source
theorem nsmul_injective_aux {A : Type v} (a : A) [add_left_cancel_monoid A] {n m : ℕ} (h : n ≤ m) (hm : m < add_order_of a) (eq : n • a = m • a) :
n = m
source
theorem nsmul_injective_of_lt_add_order_of {A : Type v} (a : A) [add_left_cancel_monoid A] {n m : ℕ} (hn : n < add_order_of a) (hm : m < add_order_of a) (eq : n • a = m • a) :
n = m
source
theorem pow_injective_of_lt_order_of {G : Type u} (x : G) {n m : ℕ} [left_cancel_monoid G] (hn : n < order_of x) (hm : m < order_of x) (eq : x ^ n = x ^ m) :
n = m
source
theorem order_of_dvd_iff_gpow_eq_one {G : Type u} {x : G} [group G] {i : ℤ} :
↑(order_of x) ∣ i ↔ x ^ i = 1
source
theorem add_order_of_dvd_iff_gsmul_eq_zero {G : Type u} {x : G} [add_group G] {i : ℤ} :
↑(add_order_of x) ∣ i ↔ i • x = 0
source
@[simp]
theorem order_of_add_subgroup {G : Type u} [add_group G] {H : add_subgroup G} (y : ↥H) :
add_order_of ↑y = add_order_of y
source
@[simp]
theorem order_of_subgroup {G : Type u} [group G] {H : subgroup G} (y : ↥H) :
order_of ↑y = order_of y
source
theorem gpow_eq_mod_order_of {G : Type u} {x : G} [group G] {i : ℤ} :
x ^ i = x ^ (i % ↑(order_of x))
source
theorem gsmul_eq_mod_add_order_of {A : Type v} {a : A} [add_group A] {i : ℤ} :
i • a = (i % ↑(add_order_of a)) • a
source
theorem pow_inj_iff_of_order_of_eq_zero {G : Type u} {x : G} [group G] (h : order_of x = 0) {n m : ℕ} :
x ^ n = x ^ m ↔ n = m
source
theorem nsmul_inj_iff_of_add_order_of_eq_zero {G : Type u} {x : G} [add_group G] (h : add_order_of x = 0) {n m : ℕ} :
n • x = m • x ↔ n = m
source
theorem pow_inj_mod {G : Type u} {x : G} [group G] {n m : ℕ} :
x ^ n = x ^ m ↔ n % order_of x = m % order_of x
source
theorem nsmul_inj_mod {A : Type v} {a : A} [add_group A] {n m : ℕ} :
n • a = m • a ↔ n % add_order_of a = m % add_order_of a
source
theorem sum_card_add_order_of_eq_card_nsmul_eq_zero {A : Type v} {n : ℕ} [fintype A] [add_monoid A] [decidable_eq A] (hn : 0 < n) :
∑ (m : ℕ) in finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ), (finset.filter (λ (a : A), add_order_of a = m) finset.univ).card = (finset.filter (λ (a : A), n • a = 0) finset.univ).card
source
theorem sum_card_order_of_eq_card_pow_eq_one {G : Type u} {n : ℕ} [fintype G] [monoid G] [decidable_eq G] (hn : 0 < n) :
∑ (m : ℕ) in finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ), (finset.filter (λ (x : G), order_of x = m) finset.univ).card = (finset.filter (λ (x : G), x ^ n = 1) finset.univ).card
source
theorem exists_pow_eq_one {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :
is_of_fin_order x
source
theorem exists_nsmul_eq_zero {A : Type v} [fintype A] [add_left_cancel_monoid A] (a : A) :
is_of_fin_add_order a
source
theorem add_order_of_le_card_univ {A : Type v} {a : A} [fintype A] [add_left_cancel_monoid A] :
add_order_of a ≤ fintype.card A
source
theorem order_of_le_card_univ {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] :
order_of x ≤ fintype.card G
source
theorem add_order_of_pos {A : Type v} [fintype A] [add_left_cancel_monoid A] (a : A) :
0 < add_order_of a

This is the same as `add_order_of_pos' but with one fewer explicit assumption since this is automatic in case of a finite cancellative additive monoid.

source
theorem order_of_pos {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :
0 < order_of x

This is the same as `order_of_pos' but with one fewer explicit assumption since this is automatic in case of a finite cancellative monoid.

source
theorem add_order_of_nsmul {A : Type v} {n : ℕ} [fintype A] [add_left_cancel_monoid A] (a : A) :
add_order_of (n • a) = add_order_of a / (add_order_of a).gcd n

This is the same as add_order_of_nsmul' and add_order_of_nsmul but with one assumption less which is automatic in the case of a finite cancellative additive monoid.

source
theorem order_of_pow {G : Type u} {n : ℕ} [fintype G] [left_cancel_monoid G] (x : G) :
order_of (x ^ n) = order_of x / (order_of x).gcd n

This is the same as order_of_pow' and order_of_pow'' but with one assumption less which is automatic in the case of a finite cancellative monoid.

source
theorem mem_multiples_iff_mem_range_add_order_of {A : Type v} {a b : A} [fintype A] [add_left_cancel_monoid A] [decidable_eq A] :
b ∈ add_submonoid.multiples a ↔ b ∈ finset.image (λ (_x : ℕ), _x • a) (finset.range (add_order_of a))
source
theorem mem_powers_iff_mem_range_order_of {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] [decidable_eq G] :
y ∈ submonoid.powers x ↔ y ∈ finset.image (pow x) (finset.range (order_of x))
source
@[instance]
def decidable_multiples {A : Type v} {a : A} [fintype A] [add_left_cancel_monoid A] [decidable_eq A] :
decidable_pred (λ (_x : A), _x ∈ add_submonoid.multiples a)
Equations
source
@[instance]
def decidable_powers {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] [decidable_eq G] :
decidable_pred (λ (_x : G), _x ∈ submonoid.powers x)
Equations
source
def fin_equiv_powers {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) :
fin (order_of x) ≃ ↥↑(submonoid.powers x)

The equivalence between fin (order_of x) and submonoid.powers x, sending i to x ^ i.

Equations
source
def fin_equiv_multiples {A : Type v} [fintype A] [add_left_cancel_monoid A] (a : A) :
fin (add_order_of a) ≃ ↥↑(add_submonoid.multiples a)

The equivalence between fin (add_order_of a) and add_submonoid.multiples a, sending i to i • a."

Equations
source
@[simp]
theorem fin_equiv_powers_apply {G : Type u} [fintype G] [left_cancel_monoid G] {x : G} {n : fin (order_of x)} :
⇑(fin_equiv_powers x) n = ⟨x ^ ↑n, _⟩
source
@[simp]
theorem fin_equiv_multiples_apply {A : Type v} [fintype A] [add_left_cancel_monoid A] {a : A} {n : fin (add_order_of a)} :
⇑(fin_equiv_multiples a) n = ⟨nsmul ↑n a, _⟩
source
@[simp]
theorem fin_equiv_powers_symm_apply {G : Type u} [fintype G] [left_cancel_monoid G] (x : G) (n : ℕ) {hn : ∃ (m : ℕ), x ^ m = x ^ n} :
⇑((fin_equiv_powers x).symm) ⟨x ^ n, hn⟩ = ⟨n % order_of x, _⟩
source
@[simp]
theorem fin_equiv_multiples_symm_apply {A : Type v} [fintype A] [add_left_cancel_monoid A] (a : A) (n : ℕ) {hn : ∃ (m : ℕ), m • a = n • a} :
⇑((fin_equiv_multiples a).symm) ⟨n • a, hn⟩ = ⟨n % add_order_of a, _⟩
source
def powers_equiv_powers {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] (h : order_of x = order_of y) :
↥↑(submonoid.powers x) ≃ ↥↑(submonoid.powers y)

The equivalence between submonoid.powers of two elements x, y of the same order, mapping x ^ i to y ^ i.

Equations
source
def multiples_equiv_multiples {A : Type v} {a b : A} [fintype A] [add_left_cancel_monoid A] (h : add_order_of a = add_order_of b) :
↥↑(add_submonoid.multiples a) ≃ ↥↑(add_submonoid.multiples b)

The equivalence between submonoid.multiples of two elements a, b of the same additive order, mapping i • a to i • b.

Equations
source
@[simp]
theorem powers_equiv_powers_apply {G : Type u} {x y : G} [fintype G] [left_cancel_monoid G] (h : order_of x = order_of y) (n : ℕ) :
⇑(powers_equiv_powers h) ⟨x ^ n, _⟩ = ⟨y ^ n, _⟩
source
@[simp]
theorem multiples_equiv_multiples_apply {A : Type v} {a b : A} [fintype A] [add_left_cancel_monoid A] (h : add_order_of a = add_order_of b) (n : ℕ) :
⇑(multiples_equiv_multiples h) ⟨n • a, _⟩ = ⟨n • b, _⟩
source
theorem order_eq_card_powers {G : Type u} {x : G} [fintype G] [left_cancel_monoid G] [decidable_eq G] :
order_of x = fintype.card ↥↑(submonoid.powers x)
source
theorem add_order_of_eq_card_multiples {A : Type v} {a : A} [fintype A] [add_left_cancel_monoid A] [decidable_eq A] :
add_order_of a = fintype.card ↥↑(add_submonoid.multiples a)
source
theorem exists_gpow_eq_one {G : Type u} [fintype G] [group G] (x : G) :
∃ (i : ℤ) (H : i ≠ 0), x ^ i = 1
source
theorem exists_gsmul_eq_zero {A : Type v} [fintype A] [add_group A] (a : A) :
∃ (i : ℤ) (H : i ≠ 0), i • a = 0
source
theorem mem_multiples_iff_mem_gmultiples {A : Type v} {a b : A} [fintype A] [add_group A] :
b ∈ add_submonoid.multiples a ↔ b ∈ add_subgroup.gmultiples a
source
theorem mem_powers_iff_mem_gpowers {G : Type u} {x y : G} [fintype G] [group G] :
y ∈ submonoid.powers x ↔ y ∈ subgroup.gpowers x
source
theorem multiples_eq_gmultiples {A : Type v} [fintype A] [add_group A] (a : A) :
↑(add_submonoid.multiples a) = ↑(add_subgroup.gmultiples a)
source
theorem powers_eq_gpowers {G : Type u} [fintype G] [group G] (x : G) :
↑(submonoid.powers x) = ↑(subgroup.gpowers x)
source
theorem mem_gmultiples_iff_mem_range_add_order_of {A : Type v} {a b : A} [fintype A] [add_group A] [decidable_eq A] :
b ∈ add_subgroup.gmultiples a ↔ b ∈ finset.image (λ (_x : ℕ), _x • a) (finset.range (add_order_of a))
source
theorem mem_gpowers_iff_mem_range_order_of {G : Type u} {x y : G} [fintype G] [group G] [decidable_eq G] :
y ∈ subgroup.gpowers x ↔ y ∈ finset.image (pow x) (finset.range (order_of x))
source
@[instance]
def decidable_gmultiples {A : Type v} {a : A} [fintype A] [add_group A] [decidable_eq A] :
decidable_pred (λ (_x : A), _x ∈ add_subgroup.gmultiples a)
Equations
source
@[instance]
def decidable_gpowers {G : Type u} {x : G} [fintype G] [group G] [decidable_eq G] :
decidable_pred (λ (_x : G), _x ∈ subgroup.gpowers x)
Equations
source
def fin_equiv_gpowers {G : Type u} [fintype G] [group G] (x : G) :
fin (order_of x) ≃ ↥↑(subgroup.gpowers x)

The equivalence between fin (order_of x) and subgroup.gpowers x, sending i to x ^ i.

Equations
source
def fin_equiv_gmultiples {A : Type v} [fintype A] [add_group A] (a : A) :
fin (add_order_of a) ≃ ↥↑(add_subgroup.gmultiples a)

The equivalence between fin (add_order_of a) and subgroup.gmultiples a, sending i to i • a.

Equations
source
@[simp]
theorem fin_equiv_gpowers_apply {G : Type u} {x : G} [fintype G] [group G] {n : fin (order_of x)} :
⇑(fin_equiv_gpowers x) n = ⟨x ^ ↑n, _⟩
source
@[simp]
theorem fin_equiv_gmultiples_apply {A : Type v} {a : A} [fintype A] [add_group A] {n : fin (add_order_of a)} :
⇑(fin_equiv_gmultiples a) n = ⟨↑n • a, _⟩
source
@[simp]
theorem fin_equiv_gpowers_symm_apply {G : Type u} [fintype G] [group G] (x : G) (n : ℕ) {hn : ∃ (m : ℤ), x ^ m = x ^ n} :
⇑((fin_equiv_gpowers x).symm) ⟨x ^ n, hn⟩ = ⟨n % order_of x, _⟩
source
@[simp]
theorem fin_equiv_gmultiples_symm_apply {A : Type v} [fintype A] [add_group A] (a : A) (n : ℕ) {hn : ∃ (m : ℤ), m • a = n • a} :
⇑((fin_equiv_gmultiples a).symm) ⟨n • a, hn⟩ = ⟨n % add_order_of a, _⟩
source
def gpowers_equiv_gpowers {G : Type u} {x y : G} [fintype G] [group G] (h : order_of x = order_of y) :
↥↑(subgroup.gpowers x) ≃ ↥↑(subgroup.gpowers y)

The equivalence between subgroup.gpowers of two elements x, y of the same order, mapping x ^ i to y ^ i.

Equations
source
def gmultiples_equiv_gmultiples {A : Type v} {a b : A} [fintype A] [add_group A] (h : add_order_of a = add_order_of b) :
↥↑(add_subgroup.gmultiples a) ≃ ↥↑(add_subgroup.gmultiples b)

The equivalence between subgroup.gmultiples of two elements a, b of the same additive order, mapping i • a to i • b.

Equations
source
@[simp]
theorem gpowers_equiv_gpowers_apply {G : Type u} {x y : G} [fintype G] [group G] (h : order_of x = order_of y) (n : ℕ) :
⇑(gpowers_equiv_gpowers h) ⟨x ^ n, _⟩ = ⟨y ^ n, _⟩
source
@[simp]
theorem gmultiples_equiv_gmultiples_apply {A : Type v} {a b : A} [fintype A] [add_group A] (h : add_order_of a = add_order_of b) (n : ℕ) :
⇑(gmultiples_equiv_gmultiples h) ⟨n • a, _⟩ = ⟨n • b, _⟩
source
theorem order_eq_card_gpowers {G : Type u} {x : G} [fintype G] [group G] [decidable_eq G] :
order_of x = fintype.card ↥↑(subgroup.gpowers x)
source
theorem add_order_eq_card_gmultiples {A : Type v} {a : A} [fintype A] [add_group A] [decidable_eq A] :
add_order_of a = fintype.card ↥↑(add_subgroup.gmultiples a)
source
theorem order_of_dvd_card_univ {G : Type u} {x : G} [fintype G] [group G] :
order_of x ∣ fintype.card G
source
theorem add_order_of_dvd_card_univ {A : Type v} {a : A} [fintype A] [add_group A] :
add_order_of a ∣ fintype.card A
source
@[simp]
theorem pow_card_eq_one {G : Type u} {x : G} [fintype G] [group G] :
x ^ fintype.card G = 1
source
@[simp]
theorem card_nsmul_eq_zero {A : Type v} [fintype A] [add_group A] {a : A} :
fintype.card A • a = 0
source
theorem nsmul_eq_mod_card {G : Type u} {x : G} [fintype G] [add_group G] (n : ℕ) :
n • x = (n % fintype.card G) • x
source
theorem pow_eq_mod_card {G : Type u} {x : G} [fintype G] [group G] (n : ℕ) :
x ^ n = x ^ (n % fintype.card G)
source
theorem gsmul_eq_mod_card {G : Type u} {x : G} [fintype G] [add_group G] (n : ℤ) :
n • x = (n % ↑(fintype.card G)) • x
source
theorem gpow_eq_mod_card {G : Type u} {x : G} [fintype G] [group G] (n : ℤ) :
x ^ n = x ^ (n % ↑(fintype.card G))
source
@[simp]
theorem pow_coprime_symm_apply {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) (g : G) :
⇑((pow_coprime h).symm) g = g ^ (fintype.card G).gcd_b n
source
def pow_coprime {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) :
G ≃ G

If gcd(|G|,n)=1 then the nth power map is a bijection

Equations
source
@[simp]
theorem pow_coprime_apply {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) (g : G) :
⇑(pow_coprime h) g = g ^ n
source
@[simp]
theorem pow_coprime_one {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) :
⇑(pow_coprime h) 1 = 1
source
@[simp]
theorem pow_coprime_inv {G : Type u} {n : ℕ} [fintype G] [group G] (h : (fintype.card G).coprime n) {g : G} :
⇑(pow_coprime h) g⁻¹ = (⇑(pow_coprime h) g)⁻¹
source
theorem inf_eq_bot_of_coprime {G : Type u_1} [group G] {H K : subgroup G} [fintype ↥H] [fintype ↥K] (h : (fintype.card ↥H).coprime (fintype.card ↥K)) :
H ⊓ K = ⊥
source
theorem image_range_add_order_of {A : Type v} (a : A) [fintype A] [add_group A] [decidable_eq A] :
finset.image (λ (i : ℕ), i • a) (finset.range (add_order_of a)) = ↑(add_subgroup.gmultiples a).to_finset
source
theorem image_range_order_of {G : Type u} {x : G} [fintype G] [group G] [decidable_eq G] :
finset.image (λ (i : ℕ), x ^ i) (finset.range (order_of x)) = ↑(subgroup.gpowers x).to_finset

TODO: Generalise to submonoid.powers.

source
theorem gcd_nsmul_card_eq_zero_iff {A : Type v} (a : A) {n : ℕ} [fintype A] [add_group A] :
n • a = 0 ↔ n.gcd (fintype.card A) • a = 0
source
theorem pow_gcd_card_eq_one_iff {G : Type u} {x : G} {n : ℕ} [fintype G] [group G] :
x ^ n = 1 ↔ x ^ n.gcd (fintype.card G) = 1

TODO: Generalise to finite_cancel_monoid.

source
def submonoid_of_idempotent {M : Type u_1} [left_cancel_monoid M] [fintype M] (S : set M) (hS1 : S.nonempty) (hS2 : S * S = S) :
submonoid M

A nonempty idempotent subset of a finite cancellative monoid is a submonoid

Equations
source
def subgroup_of_idempotent {G : Type u_1} [group G] [fintype G] (S : set G) (hS1 : S.nonempty) (hS2 : S * S = S) :
subgroup G

A nonempty idempotent subset of a finite group is a subgroup

Equations
source
def pow_card_subgroup {G : Type u_1} [group G] [fintype G] (S : set G) (hS : S.nonempty) :
subgroup G

If S is a nonempty subset of a finite group G, then S ^ |G| is a subgroup

Equations