mathlib documentation

group_theory.order_of_element

theorem finset.mem_range_iff_mem_finset_range_of_mod_eq {α : Type u_1} [decidable_eq α] {f : → α} {a : α} {n : } :
0 < n(∀ (i : ), f (i % n) = f i)(a set.range f a finset.image (λ (i : ), f i) (finset.range n))

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

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

@[instance]
def fintype_bot {α : Type u_1} [group α] :

Equations
@[simp]
theorem card_trivial {α : Type u_1} [group α] :

@[instance]
def quotient_group.fintype {α : Type u_1} [group α] [fintype α] (s : subgroup α) [d : decidable_pred (λ (a : α), a s)] :

Equations
theorem card_subgroup_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [fintype s] :

theorem card_quotient_dvd_card {α : Type u_1} [group α] [fintype α] (s : subgroup α) [decidable_pred (λ (a : α), a s)] [fintype s] :

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

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

def order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] :
α →

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

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

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

theorem pow_injective_of_lt_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n m : } (a : α) :
n < order_of am < order_of aa ^ n = a ^ mn = m

theorem order_of_le_card_univ {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

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

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

theorem mem_gpowers_iff_mem_range_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {a a' : α} :

@[instance]
def decidable_gpowers {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

Equations
theorem order_of_dvd_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : } :
a ^ n = 1order_of a n

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

theorem order_of_le_of_pow_eq_one {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] {n : } :
0 < na ^ n = 1order_of a n

theorem sum_card_order_of_eq_card_pow_eq_one {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] {n : } :
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

theorem order_eq_card_gpowers {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

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

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

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

theorem order_of_dvd_card_univ {α : Type u_1} {a : α} [group α] [fintype α] [dec : decidable_eq α] :

@[simp]
theorem pow_card_eq_one {α : Type u_1} [group α] [fintype α] (a : α) :

theorem mem_powers_iff_mem_gpowers {α : Type u_1} [group α] [fintype α] {a x : α} :

theorem powers_eq_gpowers {α : Type u_1} [group α] [fintype α] (a : α) :

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

theorem image_range_order_of {α : Type u_1} [group α] [fintype α] [dec : decidable_eq α] (a : α) :

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

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

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

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

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

Equations
theorem is_cyclic_of_order_of_eq_card {α : Type u_1} [group α] [decidable_eq α] [fintype α] (x : α) :

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

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

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

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

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

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

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

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

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 : } :
d fintype.card α(finset.filter (λ (a : α), order_of a = d) finset.univ).card = d.totient

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

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