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 #

Tags #

cyclic group

@[class]
structure is_add_cyclic (α : Type u) [add_group α] :
Prop

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

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

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

Instances
@[protected, instance]
def is_cyclic_of_subsingleton {α : Type u} [group α] [subsingleton α] :
@[protected, instance]
def is_add_cyclic.add_comm_group {α : Type u} [hg : add_group α] [is_add_cyclic α] :

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
theorem monoid_add_hom.map_add_cyclic {G : Type u_1} [add_group G] [h : is_add_cyclic G] (σ : G →+ G) :
∃ (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 : add_order_of x = fintype.card α) :
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 is_add_cyclic_of_prime_card {α : Type u} [add_group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : fintype.card α = p) :
theorem add_order_of_eq_card_of_forall_mem_zmultiples {α : Type u} [add_group α] [fintype α] {g : α} (hx : ∀ (x : α), x add_subgroup.zmultiples g) :
theorem order_of_eq_card_of_forall_mem_zpowers {α : Type u} [group α] [fintype α] {g : α} (hx : ∀ (x : α), x subgroup.zpowers g) :
theorem infinite.order_of_eq_zero_of_forall_mem_zpowers {α : Type u} [group α] [infinite α] {g : α} (h : ∀ (x : α), x subgroup.zpowers g) :
theorem infinite.add_order_of_eq_zero_of_forall_mem_zmultiples {α : Type u} [add_group α] [infinite α] {g : α} (h : ∀ (x : α), x add_subgroup.zmultiples g) :
@[protected, instance]
def bot.is_add_cyclic {α : Type u} [add_group α] :
@[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 α] [is_add_cyclic α] {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
theorem is_add_cyclic.exists_add_monoid_generator {α : Type u} [add_group α] [fintype α] [is_add_cyclic α] :
∃ (x : α), ∀ (y : α), y add_submonoid.multiples x
theorem is_cyclic.exists_monoid_generator {α : Type u} [group α] [fintype α] [is_cyclic α] :
∃ (x : α), ∀ (y : α), y submonoid.powers x
theorem is_add_cyclic.image_range_order_of {α : Type u} {a : α} [add_group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x add_subgroup.zmultiples a) :
theorem is_cyclic.image_range_order_of {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x subgroup.zpowers a) :
theorem is_cyclic.image_range_card {α : Type u} {a : α} [group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x subgroup.zpowers a) :
theorem is_add_cyclic.image_range_card {α : Type u} {a : α} [add_group α] [decidable_eq α] [fintype α] (ha : ∀ (x : α), x add_subgroup.zmultiples 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_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 fintype.card α) :
theorem is_add_cyclic.card_order_of_eq_totient {α : Type u_1} [add_group α] [is_add_cyclic α] [fintype α] {d : } (hd : d fintype.card α) :
theorem is_simple_add_group_of_prime_card {α : Type u} [add_group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : fintype.card α = p) :
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_add_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] [is_add_cyclic H] (f : G →+ H) (hf : f.ker add_subgroup.center G) (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 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
def commutative_of_add_cycle_center_quotient {G : Type u_1} {H : Type u_2} [add_group G] [add_group H] [is_add_cyclic H] (f : G →+ H) (hf : f.ker add_subgroup.center G) :

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

Equations
@[protected, instance]
@[protected, instance]
theorem is_cyclic.exponent_eq_card {α : Type u} [group α] [is_cyclic α] [fintype α] :