# mathlibdocumentation

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 #

• is_cyclic is a predicate on a group stating that the group is cyclic.

## Main statements #

• is_cyclic_of_prime_card proves that a finite group of prime order is cyclic.
• is_simple_group_of_prime_card, is_simple_group.is_cyclic, and is_simple_group.prime_card classify finite simple abelian groups.

## Implementation details #

This file is currently only available for multiplicatively written groups.

cyclic group

## TODO #

• Add the attribute @[to_additive] to the declarations about is_cyclic, so that they work for additive groups.
@[class]
structure is_cyclic (α : Type u) [group α] :
Prop
• exists_generator : ∃ (g : α), ∀ (x : α),

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 : = ) :
theorem is_cyclic_of_prime_card {α : Type u} [group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : = 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 : α), ) :
@[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 : α),
theorem is_cyclic.image_range_order_of {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), ) :
theorem is_cyclic.image_range_card {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), ) :
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 ^ = 1) finset.univ).card =
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 ) :
(finset.filter (λ (a : α), = d) finset.univ).card = d.totient
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 ) :
(finset.filter (λ (a : α), = d) finset.univ).card = d.totient
theorem is_simple_group_of_prime_card {α : Type u} [group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : = 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 ) (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 ) :

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

Equations
@[instance]
def is_simple_group.is_cyclic {α : Type u} [comm_group α]  :
theorem is_simple_group.prime_card {α : Type u} [comm_group α] [fintype α] :