Documentation

Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic

Cyclic groups #

This file develops basic properties of cyclic groups that only require minimal imports.

Note that IsCyclic is a predicate on a group stating that the group is cyclic. For the concrete cyclic group of order n, see Data.ZMod.Basic.

source
instance instIsAddCyclicInt :
IsAddCyclic ℤ
source
@[instance 100]
instance isCyclic_of_subsingleton {α : Type u_1} [Group α] [Subsingleton α] :
IsCyclic α
source
@[instance 100]
instance isAddCyclic_of_subsingleton {α : Type u_1} [AddGroup α] [Subsingleton α] :
IsAddCyclic α
source
@[simp]
theorem isCyclic_multiplicative_iff {α : Type u_1} [SubNegMonoid α] :
IsCyclic (Multiplicative α) ↔ IsAddCyclic α
source
instance isCyclic_multiplicative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :
IsCyclic (Multiplicative α)
source
@[simp]
theorem isAddCyclic_additive_iff {α : Type u_1} [DivInvMonoid α] :
IsAddCyclic (Additive α) ↔ IsCyclic α
source
instance isAddCyclic_additive {α : Type u_1} [Group α] [IsCyclic α] :
IsAddCyclic (Additive α)
source
instance IsCyclic.isMulCommutative {α : Type u_1} [Group α] [IsCyclic α] :
IsMulCommutative α
source
instance IsAddCyclic.isAddCommutative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :
IsAddCommutative α
source
@[deprecated IsAddCyclic.isAddCommutative (since := "2026-04-09")]
theorem IsAddCyclic.commutative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :
IsAddCommutative α

Alias of IsAddCyclic.isAddCommutative.

source
@[deprecated IsCyclic.isMulCommutative (since := "2026-04-09")]
theorem IsCyclic.commutative {α : Type u_1} [Group α] [IsCyclic α] :
IsMulCommutative α

Alias of IsCyclic.isMulCommutative.

source
@[instance_reducible]
def IsCyclic.commGroup {α : Type u_1} [Group α] [IsCyclic α] :
CommGroup α

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

Equations
Instances For
    source
    @[instance_reducible]
    def IsAddCyclic.addCommGroup {α : Type u_1} [AddGroup α] [IsAddCyclic α] :
    AddCommGroup α

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

    Equations
    Instances For
      source
      theorem Nontrivial.of_not_isCyclic {α : Type u_1} [Group α] (nc : ¬IsCyclic α) :
      Nontrivial α

      A non-cyclic multiplicative group is non-trivial.

      source
      theorem Nontrivial.of_not_isAddCyclic {α : Type u_1} [AddGroup α] (nc : ¬IsAddCyclic α) :
      Nontrivial α

      A non-cyclic additive group is non-trivial.

      source
      theorem MonoidHom.map_cyclic {G : Type u_2} [Group G] [h : IsCyclic G] (σ : G →* G) :
      ∃ (m : ℤ), ∀ (g : G), σ g = g ^ m
      source
      theorem AddMonoidHom.map_addCyclic {G : Type u_2} [AddGroup G] [h : IsAddCyclic G] (σ : G →+ G) :
      ∃ (m : ℤ), ∀ (g : G), σ g = m • g
      source
      theorem isCyclic_of_surjective {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {F : Type u_4} [hH : IsCyclic G'] [FunLike F G' G] [MonoidHomClass F G' G] (f : F) (hf : Function.Surjective ⇑f) :
      IsCyclic G
      source
      theorem isAddCyclic_of_surjective {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {F : Type u_4} [hH : IsAddCyclic G'] [FunLike F G' G] [AddMonoidHomClass F G' G] (f : F) (hf : Function.Surjective ⇑f) :
      IsAddCyclic G
      source
      theorem MulEquiv.isCyclic {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] (e : G ≃* G') :
      IsCyclic G ↔ IsCyclic G'
      source
      theorem AddEquiv.isAddCyclic {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] (e : G ≃+ G') :
      IsAddCyclic G ↔ IsAddCyclic G'