# Documentation

Mathlib.GroupTheory.SpecificGroups.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 #

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

## Main statements #

• isCyclic_of_prime_card proves that a finite group of prime order is cyclic.
• isSimpleGroup_of_prime_card, IsSimpleGroup.isCyclic, and IsSimpleGroup.prime_card classify finite simple abelian groups.
• IsCyclic.exponent_eq_card: For a finite cyclic group G, the exponent is equal to the group's cardinality.
• IsCyclic.exponent_eq_zero_of_infinite: Infinite cyclic groups have exponent zero.
• IsCyclic.iff_exponent_eq_card: A finite commutative group is cyclic iff its exponent is equal to its cardinality.

## Tags #

cyclic group

class IsAddCyclic (α : Type u) [] :
• exists_generator : g, ∀ (x : α),

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

Instances
class IsCyclic (α : Type u) [] :
• exists_generator : g, ∀ (x : α),

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

Instances
instance isAddCyclic_of_subsingleton {α : Type u} [] [] :
instance isCyclic_of_subsingleton {α : Type u} [] [] :
abbrev IsAddCyclic.addCommGroup.match_2 {α : Type u_1} [hg : ] (motive : (g, ∀ (x : α), ) → Prop) :
(x : g, ∀ (x : α), ) → ((w : α) → (hg : ∀ (x : α), ) → motive (_ : g, ∀ (x : α), )) → motive x
Instances For
theorem IsAddCyclic.addCommGroup.proof_1 {α : Type u_1} [hg : ] [] (x : α) (y : α) :
x + y = y + x

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

Instances For
abbrev IsAddCyclic.addCommGroup.match_1 {α : Type u_1} [hg : ] (y : α) :
(w : α) → ∀ (motive : ) (x : ), (∀ (w_1 : ) (hm : (fun x x_1 => x_1 x) w w_1 = y), motive (_ : y, (fun x x_1 => x_1 x) w y = y)) → motive x
Instances For
def IsCyclic.commGroup {α : Type u} [hg : ] [] :

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

Instances For
theorem MonoidAddHom.map_add_cyclic {G : Type u_1} [] [h : ] (σ : G →+ G) :
m, ∀ (g : G), σ g = m g
theorem MonoidHom.map_cyclic {G : Type u_1} [] [h : ] (σ : G →* G) :
m, ∀ (g : G), σ g = g ^ m
theorem isAddCyclic_of_orderOf_eq_card {α : Type u} [] [] (x : α) (hx : ) :
theorem isCyclic_of_orderOf_eq_card {α : Type u} [] [] (x : α) (hx : ) :
theorem isAddCyclic_of_prime_card {α : Type u} [] [] {p : } [hp : Fact ()] (h : ) :

A finite group of prime order is cyclic.

theorem isCyclic_of_prime_card {α : Type u} [] [] {p : } [hp : Fact ()] (h : ) :

A finite group of prime order is cyclic.

theorem addOrderOf_eq_card_of_forall_mem_zmultiples {α : Type u} [] [] {g : α} (hx : ∀ (x : α), ) :
theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u} [] [] {g : α} (hx : ∀ (x : α), ) :
theorem Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples {α : Type u} [] [] {g : α} (h : ∀ (x : α), ) :
= 0
theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers {α : Type u} [] [] {g : α} (h : ∀ (x : α), ) :
= 0
instance Bot.isAddCyclic {α : Type u} [] :
IsAddCyclic { x // x }
theorem Bot.isAddCyclic.proof_1 {α : Type u_1} [] :
IsAddCyclic { x // x }
instance Bot.isCyclic {α : Type u} [] :
IsCyclic { x // x }
abbrev AddSubgroup.isAddCyclic.match_1 {α : Type u_1} [] (g : α) (x : α) (motive : ) :
(x : ) → ((k : ) → (hk : (fun x x_1 => x_1 x) g k = x) → motive (_ : y, (fun x x_1 => x_1 x) g y = x)) → motive x
Instances For
instance AddSubgroup.isAddCyclic {α : Type u} [] [] (H : ) :
IsAddCyclic { x // x H }
abbrev AddSubgroup.isAddCyclic.match_3 {α : Type u_1} [] (H : ) (motive : (x, x H x 0) → Prop) :
(hx : x, x H x 0) → ((x : α) → (hx₁ : x H) → (hx₂ : x 0) → motive (_ : x, x H x 0)) → motive hx
Instances For
theorem AddSubgroup.isAddCyclic.proof_1 {α : Type u_1} [] [] (H : ) :
IsAddCyclic { x // x H }
abbrev AddSubgroup.isAddCyclic.match_2 {α : Type u_1} [] (H : ) (motive : { x // x H }Prop) :
(x : { x // x H }) → ((x : α) → (hx : x H) → motive { val := x, property := hx }) → motive x
Instances For
instance Subgroup.isCyclic {α : Type u} [] [] (H : ) :
IsCyclic { x // x H }
abbrev IsAddCyclic.card_pow_eq_one_le.match_2 {α : Type u_1} [] {n : } (motive : Nat.gcd n () Prop) :
(x : Nat.gcd n () ) → ((m : ) → (hm : = Nat.gcd n () * m) → motive (_ : c, = Nat.gcd n () * c)) → motive x
Instances For
abbrev IsAddCyclic.card_pow_eq_one_le.match_1 {α : Type u_1} [] (g : α) (x : α) (motive : ) :
(x : ) → ((m : ) → (hm : (fun x x_1 => x_1 x) g m = x) → motive (_ : y, (fun x x_1 => x_1 x) g y = x)) → motive x
Instances For
theorem IsAddCyclic.card_pow_eq_one_le {α : Type u} [] [] [] [] {n : } (hn0 : 0 < n) :
Finset.card (Finset.filter (fun a => n a = 0) Finset.univ) n
theorem IsCyclic.card_pow_eq_one_le {α : Type u} [] [] [] [] {n : } (hn0 : 0 < n) :
Finset.card (Finset.filter (fun a => a ^ n = 1) Finset.univ) n
x, ∀ (y : α),
theorem IsCyclic.exists_monoid_generator {α : Type u} [] [] [] :
x, ∀ (y : α),
theorem IsAddCyclic.image_range_addOrderOf {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun i => i a) () = Finset.univ
theorem IsCyclic.image_range_orderOf {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun i => a ^ i) () = Finset.univ
theorem IsAddCyclic.image_range_card {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun i => i a) () = Finset.univ
theorem IsCyclic.image_range_card {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun i => a ^ i) () = Finset.univ
theorem card_orderOf_eq_totient_aux₂ {α : Type u} [] [] [] (hn : ∀ (n : ), 0 < nFinset.card (Finset.filter (fun a => a ^ n = 1) Finset.univ) n) {d : } (hd : ) :
Finset.card (Finset.filter (fun a => = d) Finset.univ) =
theorem isCyclic_of_card_pow_eq_one_le {α : Type u} [] [] [] (hn : ∀ (n : ), 0 < nFinset.card (Finset.filter (fun a => a ^ n = 1) Finset.univ) n) :
theorem isAddCyclic_of_card_pow_eq_one_le {α : Type u_1} [] [] [] (hn : ∀ (n : ), 0 < nFinset.card (Finset.filter (fun a => n a = 0) Finset.univ) n) :
theorem IsCyclic.card_orderOf_eq_totient {α : Type u} [] [] [] {d : } (hd : ) :
Finset.card (Finset.filter (fun a => = d) Finset.univ) =
theorem IsAddCyclic.card_orderOf_eq_totient {α : Type u_1} [] [] [] {d : } (hd : ) :
Finset.card (Finset.filter (fun a => = d) Finset.univ) =
theorem isSimpleAddGroup_of_prime_card {α : Type u} [] [] {p : } [hp : Fact ()] (h : ) :

A finite group of prime order is simple.

theorem isSimpleGroup_of_prime_card {α : Type u} [] [] {p : } [hp : Fact ()] (h : ) :

A finite group of prime order is simple.

abbrev commutative_of_add_cyclic_center_quotient.match_1 {G : Type u_2} {H : Type u_1} [] [] (f : G →+ H) (b : G) (x : H) (y : G) (hxy : f y = x) (motive : { val := f b, property := (_ : y, f y = f b) } AddSubgroup.zmultiples { val := x, property := (_ : y, f y = x) }Prop) :
(x : { val := f b, property := (_ : y, f y = f b) } AddSubgroup.zmultiples { val := x, property := (_ : y, f y = x) }) → ((n : ) → (hn : (fun x x_1 => x_1 x) { val := x, property := (_ : y, f y = x) } n = { val := f b, property := (_ : y, f y = f b) }) → motive (_ : y, (fun x x_1 => x_1 x) { val := x, property := (_ : y, f y = x) } y = { val := f b, property := (_ : y, f y = f b) })) → motive x
Instances For
abbrev commutative_of_add_cyclic_center_quotient.match_2 {G : Type u_2} {H : Type u_1} [] [] (f : G →+ H) (motive : (g, ∀ (x : { x // }), ) → Prop) :
(x : g, ∀ (x : { x // }), ) → ((x : H) → (y : G) → (hxy : f y = x) → (hx : ∀ (a : { x // }), a AddSubgroup.zmultiples { val := x, property := (_ : y, f y = x) }) → motive (_ : g, ∀ (x : { x // }), )) → motive x
Instances For
theorem commutative_of_add_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [] [] [] (f : G →+ H) (hf : ) (a : G) (b : G) :
a + b = b + a

A group is commutative if the quotient by the center is cyclic. Also see addCommGroup_of_cycle_center_quotient for the AddCommGroup instance.

theorem commutative_of_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [] [] [] (f : G →* H) (hf : ) (a : G) (b : G) :
a * b = b * a

A group is commutative if the quotient by the center is cyclic. Also see commGroup_of_cycle_center_quotient for the CommGroup instance.

def commutativeOfAddCycleCenterQuotient {G : Type u_1} {H : Type u_2} [] [] [] (f : G →+ H) (hf : ) :

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

Instances For
def commGroupOfCycleCenterQuotient {G : Type u_1} {H : Type u_2} [] [] [] (f : G →* H) (hf : ) :

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

Instances For