# 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.
• is_cyclic.exponent_eq_card: For a finite cyclic group G, the exponent is equal to the group's cardinality.
• is_cyclic.exponent_eq_zero_of_infinite: Infinite cyclic groups have exponent zero.
• is_cyclic.iff_exponent_eq_card: A finite commutative group is cyclic iff its exponent is equal to its cardinality.

## Tags #

cyclic group

@[class]
Prop
• exists_generator : ∃ (g : α), ∀ (x : α),

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

Instances of this typeclass
@[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 of this typeclass
@[protected, instance]
def is_cyclic_of_subsingleton {α : Type u} [group α] [subsingleton α] :
@[protected, instance]

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

Equations
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
∃ (m : ), ∀ (g : G), σ g = m g
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_add_cyclic_of_order_of_eq_card {α : Type u} [add_group α] [fintype α] (x : α) (hx : = ) :
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 is_add_cyclic_of_prime_card {α : Type u} [add_group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : = p) :

A finite group of prime order is cyclic.

theorem add_order_of_eq_card_of_forall_mem_zmultiples {α : Type u} [add_group α] [fintype α] {g : α} (hx : ∀ (x : α), ) :
theorem order_of_eq_card_of_forall_mem_zpowers {α : Type u} [group α] [fintype α] {g : α} (hx : ∀ (x : α), ) :
theorem infinite.order_of_eq_zero_of_forall_mem_zpowers {α : Type u} [group α] [infinite α] {g : α} (h : ∀ (x : α), ) :
= 0
theorem infinite.add_order_of_eq_zero_of_forall_mem_zmultiples {α : Type u} [add_group α] [infinite α] {g : α} (h : ∀ (x : α), ) :
@[protected, instance]
@[protected, instance]
def bot.is_cyclic {α : Type u} [group α] :
@[protected, instance]
def subgroup.is_cyclic {α : Type u} [group α] [is_cyclic α] (H : subgroup α) :
@[protected, instance]
theorem is_add_cyclic.card_pow_eq_one_le {α : Type u} [add_group α] [decidable_eq α] [fintype α] {n : } (hn0 : 0 < n) :
(finset.filter (λ (a : α), n a = 0) finset.univ).card n
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
∃ (x : α), ∀ (y : α),
theorem is_cyclic.exists_monoid_generator {α : Type u} [group α] [finite α] [is_cyclic α] :
∃ (x : α), ∀ (y : α),
theorem is_add_cyclic.image_range_order_of {α : Type u} {a : α} [add_group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), ) :
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 is_add_cyclic.image_range_card {α : Type u} {a : α} [add_group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), ) :
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_add_cyclic_of_card_pow_eq_one_le {α : Type u_1} [add_group α] [decidable_eq α] [fintype α] (hn : ∀ (n : ), 0 < n(finset.filter (λ (a : α), n a = 0) 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_add_cyclic.card_order_of_eq_totient {α : Type u_1} [add_group α] [fintype α] {d : } (hd : d ) :
(finset.filter (λ (a : α), = d) finset.univ).card = d.totient
theorem is_simple_add_group_of_prime_card {α : Type u} [add_group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : = p) :

A finite group of prime order is simple.

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_add_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [add_group G] [add_group 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 add_comm_group_of_cycle_center_quotient for the add_comm_group instance.

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
def commutative_of_add_cycle_center_quotient {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] (f : G →+ H) (hf : f.ker ) :

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

Equations
@[protected, instance]