mathlib3 documentation

group_theory.specific_groups.cyclic

Cyclic groups #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 of this typeclass
@[class]
structure is_cyclic (α : Type u) [group α] :
Prop

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

Instances of this typeclass
@[protected, instance]
@[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
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_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) :

A finite group of prime order is cyclic.

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) :
@[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 α] [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_cyclic.exists_monoid_generator {α : Type u} [group α] [finite α] [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_simple_add_group_of_prime_card {α : Type u} [add_group α] [fintype α] {p : } [hp : fact (nat.prime p)] (h : fintype.card α = 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 : 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

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

Equations
@[protected, instance]