mathlib documentation

group_theory.order_of_element

source
theorem finset.mem_range_iff_mem_finset_range_of_mod_eq {α : Type u_1} [decidable_eq α] {f : ℤ → α} {a : α} {n : ℕ} (hn : 0 < n) (h : ∀ (i : ℤ), f (i % ↑n) = f i) :
a ∈ set.range f ↔ a ∈ finset.image (λ (i : ℕ), f ↑i) (finset.range n)

source
theorem conj_injective {α : Type u_1} [group α] {x : α} :
function.injective (λ (g : α), (x * g) * x⁻¹)

source
theorem mem_normalizer_fintype {α : Type u_1} [group α] {s : set α} [fintype ↥s] {x : α} (h : ∀ (n : α), n ∈ s → (x * n) * x⁻¹ ∈ s) :
x ∈ subgroup.set_normalizer s

source
@[instance]
def fintype_bot {α : Type u_1} [group α] :
fintype ↥⊥

Equations
source
@[simp]
theorem card_trivial {α : Type u_1} [group α] :
fintype.card ↥⊥ = 1

source
theorem card_eq_card_quotient_mul_card_subgroup {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype ↥s] [decidable_pred (λ (a : α), a ∈ s)] :
fintype.card α = (fintype.card (quotient_group.quotient s)) * fintype.card ↥s

source
theorem card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype ↥s] :
fintype.card ↥s ∣ fintype.card α

source
theorem card_quotient_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [decidable_pred (λ (a : α), a ∈ s)] [fintype ↥s] :
fintype.card (quotient_group.quotient s) ∣ fintype.card α

source
theorem exists_gpow_eq_one {α : Type u_1} [group α] [fintype α] (a : α) :
∃ (i : ℤ) (H : i ≠ 0), a ^ i = 1

source
theorem exists_pow_eq_one {α : Type u_1} [group α] [fintype α] (a : α) :
∃ (i : ℕ) (H : i > 0), a ^ i = 1

source
def order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :
ℕ

order_of a is the order of the element a, i.e. the n ≥ 1, s.t. a ^ n = 1

Equations
source
theorem pow_order_of_eq_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :
a ^ order_of a = 1

source
theorem order_of_pos {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :
0 < order_of a

source
theorem pow_injective_of_lt_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n m : ℕ} (a : α) (hn : n < order_of a) (hm : m < order_of a) (eq : a ^ n = a ^ m) :
n = m

source
theorem order_of_le_card_univ {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :
order_of a ≤ fintype.card α

source
theorem pow_eq_mod_order_of {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} :
a ^ n = a ^ (n % order_of a)

source
theorem gpow_eq_mod_order_of {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {i : ℤ} :
a ^ i = a ^ (i % ↑(order_of a))

source
theorem mem_gpowers_iff_mem_range_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {a a' : α} :
a' ∈ subgroup.gpowers a ↔ a' ∈ finset.image (pow a) (finset.range (order_of a))

source
@[instance]
def decidable_gpowers {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :
decidable_pred ↑(subgroup.gpowers a)

Equations
source
theorem order_of_dvd_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} (h : a ^ n = 1) :
order_of a ∣ n

source
theorem order_of_dvd_iff_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} :
order_of a ∣ n ↔ a ^ n = 1

source
theorem order_of_le_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} (hn : 0 < n) (h : a ^ n = 1) :
order_of a ≤ n

source
theorem sum_card_order_of_eq_card_pow_eq_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n : ℕ} (hn : 0 < n) :
∑ (m : ℕ) in finset.filter (λ (_x : ℕ), _x ∣ n) (finset.range n.succ), (finset.filter (λ (a : α), order_of a = m) finset.univ).card = (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card

source
theorem order_eq_card_gpowers {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :
order_of a = fintype.card ↥↑(subgroup.gpowers a)

source
@[simp]
theorem order_of_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] :
order_of 1 = 1

source
@[simp]
theorem order_of_eq_one_iff {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :
order_of a = 1 ↔ a = 1

source
theorem order_of_eq_prime {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {p : ℕ} [hp : fact (nat.prime p)] (hg : a ^ p = 1) (hg1 : a ≠ 1) :
order_of a = p

source
theorem order_of_dvd_card_univ {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :
order_of a ∣ fintype.card α

source
@[simp]
theorem pow_card_eq_one {α : Type u_1} [group α] [fintype α] (a : α) :
a ^ fintype.card α = 1

source
theorem mem_powers_iff_mem_gpowers {α : Type u_1} [group α] [fintype α] {a x : α} :
x ∈ submonoid.powers a ↔ x ∈ subgroup.gpowers a

source
theorem powers_eq_gpowers {α : Type u_1} [group α] [fintype α] (a : α) :
↑(submonoid.powers a) = ↑(subgroup.gpowers a)

source
theorem order_of_pow {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) (n : ℕ) :
order_of (a ^ n) = order_of a / (order_of a).gcd n

source
theorem image_range_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :
finset.image (λ (i : ℕ), a ^ i) (finset.range (order_of a)) = ↑(subgroup.gpowers a).to_finset

source
theorem pow_gcd_card_eq_one_iff {α : Type u_1} [group α] [fintype α] {n : ℕ} {a : α} :
a ^ n = 1 ↔ a ^ n.gcd (fintype.card α) = 1

source
@[class]
structure is_cyclic (α : Type u_2) [group α] :
Prop

A group is called cyclic if it is generated by a single element.

Instances
source
def is_cyclic.comm_group {α : Type u_1} [hg : group α] [is_cyclic α] :
comm_group α

A cyclic group is always commutative. This is not an instance because often we have a better proof of comm_group.

Equations
source
theorem is_cyclic_of_order_of_eq_card {α : Type u_1} [group α] [decidable_eq α] [fintype α] (x : α) (hx : order_of x = fintype.card α) :
is_cyclic α

source
theorem is_cyclic_of_prime_card {α : Type u_1} [group α] [fintype α] {p : ℕ} [hp : fact (nat.prime p)] (h : fintype.card α = p) :
is_cyclic α

source
theorem order_of_eq_card_of_forall_mem_gpowers {α : Type u_1} [group α] [decidable_eq α] [fintype α] {g : α} (hx : ∀ (x : α), x ∈ subgroup.gpowers g) :
order_of g = fintype.card α

source
@[instance]
def bot.is_cyclic {α : Type u_1} [group α] :
is_cyclic ↥⊥

source
@[instance]
def subgroup.is_cyclic {α : Type u_1} [group α] [is_cyclic α] (H : subgroup α) :
is_cyclic ↥H

source
theorem is_cyclic.card_pow_eq_one_le {α : Type u_1} [group α] [decidable_eq α] [fintype α] [is_cyclic α] {n : ℕ} (hn0 : 0 < n) :
(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n

source
theorem is_cyclic.exists_monoid_generator (α : Type u_1) [group α] [fintype α] [is_cyclic α] :
∃ (x : α), ∀ (y : α), y ∈ submonoid.powers x

source
theorem is_cyclic.image_range_order_of {α : Type u_1} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x ∈ subgroup.gpowers a) :
finset.image (λ (i : ℕ), a ^ i) (finset.range (order_of a)) = finset.univ

source
theorem is_cyclic.image_range_card {α : Type u_1} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x ∈ subgroup.gpowers a) :
finset.image (λ (i : ℕ), a ^ i) (finset.range (fintype.card α)) = finset.univ

source
theorem card_pow_eq_one_eq_order_of_aux {α : Type u_1} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ℕ), 0 < n → (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n) (a : α) :
(finset.filter (λ (b : α), b ^ order_of a = 1) finset.univ).card = order_of a

source
theorem card_order_of_eq_totient_aux₂ {α : Type u_1} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ℕ), 0 < n → (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n) {d : ℕ} (hd : d ∣ fintype.card α) :
(finset.filter (λ (a : α), order_of a = d) finset.univ).card = d.totient

source
theorem is_cyclic_of_card_pow_eq_one_le {α : Type u_1} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ℕ), 0 < n → (finset.filter (λ (a : α), a ^ n = 1) finset.univ).card ≤ n) :
is_cyclic α

source
theorem is_cyclic.card_order_of_eq_totient {α : Type u_1} [group α] [is_cyclic α] [decidable_eq α] [fintype α] {d : ℕ} (hd : d ∣ fintype.card α) :
(finset.filter (λ (a : α), order_of a = d) finset.univ).card = d.totient