mathlib documentation

group_theory.specific_groups.cyclic

Cyclic groups #

A group G is called cyclic if there exists an element g : G such that every element of G is of the form g ^ n for some n : ℕ. This file only deals with the predicate on a group to be cyclic. For the concrete cyclic group of order n, see data.zmod.basic.

Main definitions #

Main statements #

Implementation details #

This file is currently only available for multiplicatively written groups.

Tags #

cyclic group

TODO #

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

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

Instances
@[instance]
def is_cyclic_of_subsingleton {α : Type u} [group α] [subsingleton α] :
def is_cyclic.comm_group {α : Type u} [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 monoid_hom.map_cyclic {G : Type u_1} [group G] [h : is_cyclic G] (σ : G →* G) :
∃ (m : ), ∀ (g : G), σ g = g ^ m
theorem is_cyclic_of_order_of_eq_card {α : Type u} [group α] [fintype α] (x : α) (hx : order_of x = fintype.card α) :
theorem is_cyclic_of_prime_card {α : Type u} [group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : fintype.card α = p) :

A finite group of prime order is cyclic.

theorem order_of_eq_card_of_forall_mem_gpowers {α : Type u} [group α] [fintype α] {g : α} (hx : ∀ (x : α), x subgroup.gpowers g) :
@[instance]
def bot.is_cyclic {α : Type u} [group α] :
@[instance]
def subgroup.is_cyclic {α : Type u} [group α] [is_cyclic α] (H : subgroup α) :
theorem is_cyclic.card_pow_eq_one_le {α : Type u} [group α] [decidable_eq α] [fintype α] [is_cyclic α] {n : } (hn0 : 0 < n) :
(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card n
theorem is_cyclic.exists_monoid_generator {α : Type u} [group α] [fintype α] [is_cyclic α] :
∃ (x : α), ∀ (y : α), y submonoid.powers x
theorem is_cyclic.image_range_order_of {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x subgroup.gpowers a) :
theorem is_cyclic.image_range_card {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x subgroup.gpowers a) :
theorem card_pow_eq_one_eq_order_of_aux {α : Type u} [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} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ), 0 < n(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card n) {d : } (hd : d fintype.card α) :
theorem is_cyclic_of_card_pow_eq_one_le {α : Type u} [group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ), 0 < n(finset.filter (λ (a : α), a ^ n = 1) finset.univ).card n) :
theorem is_cyclic.card_order_of_eq_totient {α : Type u} [group α] [is_cyclic α] [fintype α] {d : } (hd : d fintype.card α) :
theorem is_simple_group_of_prime_card {α : Type u} [group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : fintype.card α = p) :

A finite group of prime order is simple.

theorem commutative_of_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [group G] [group H] [is_cyclic H] (f : G →* H) (hf : f.ker subgroup.center G) (a b : G) :
a * b = b * a

A group is commutative if the quotient by the center is cyclic. Also see comm_group_of_cycle_center_quotient for the comm_group instance

def comm_group_of_cycle_center_quotient {G : Type u_1} {H : Type u_2} [group G] [group H] [is_cyclic H] (f : G →* H) (hf : f.ker subgroup.center G) :

A group is commutative if the quotient by the center is cyclic.

Equations
@[instance]