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 #

Main statements #

Tags #

cyclic group

theorem IsCyclic.exists_generator {α : Type u_1} [Group α] [IsCyclic α] :
∃ (g : α), ∀ (x : α), x Subgroup.zpowers g
theorem IsAddCyclic.exists_generator {α : Type u_1} [AddGroup α] [IsAddCyclic α] :
∃ (g : α), ∀ (x : α), x AddSubgroup.zmultiples g
theorem Subgroup.isCyclic_iff_exists_zpowers_eq_top {α : Type u_1} [Group α] (H : Subgroup α) :
IsCyclic H ∃ (g : α), zpowers g = H
@[instance 100]
instance isCyclic_of_subsingleton {α : Type u_1} [Group α] [Subsingleton α] :
@[instance 100]
instance IsCyclic.commutative {α : Type u_1} [Group α] [IsCyclic α] :
Std.Commutative fun (x1 x2 : α) => x1 * x2
instance IsAddCyclic.commutative {α : Type u_1} [AddGroup α] [IsAddCyclic α] :
Std.Commutative fun (x1 x2 : α) => x1 + x2
def IsCyclic.commGroup {α : Type u_1} [hg : Group α] [IsCyclic α] :

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

Equations
Instances For

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

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

      A non-cyclic multiplicative group is non-trivial.

      A non-cyclic additive group is non-trivial.

      theorem MonoidHom.map_cyclic {G : Type u_2} [Group G] [h : IsCyclic G] (σ : G →* G) :
      ∃ (m : ), ∀ (g : G), σ g = g ^ m
      theorem AddMonoidHom.map_addCyclic {G : Type u_2} [AddGroup G] [h : IsAddCyclic G] (σ : G →+ G) :
      ∃ (m : ), ∀ (g : G), σ g = m g
      theorem isCyclic_iff_exists_orderOf_eq_natCard {α : Type u_1} [Group α] [Finite α] :
      IsCyclic α ∃ (g : α), orderOf g = Nat.card α
      theorem isCyclic_iff_exists_natCard_le_orderOf {α : Type u_1} [Group α] [Finite α] :
      IsCyclic α ∃ (g : α), Nat.card α orderOf g
      @[deprecated isCyclic_iff_exists_orderOf_eq_natCard (since := "2024-12-20")]
      theorem isCyclic_iff_exists_ofOrder_eq_natCard {α : Type u_1} [Group α] [Finite α] :
      IsCyclic α ∃ (g : α), orderOf g = Nat.card α

      Alias of isCyclic_iff_exists_orderOf_eq_natCard.

      @[deprecated isAddCyclic_iff_exists_addOrderOf_eq_natCard (since := "2024-12-20")]

      Alias of isAddCyclic_iff_exists_addOrderOf_eq_natCard.

      @[deprecated isCyclic_iff_exists_orderOf_eq_natCard (since := "2024-12-20")]

      Alias of isCyclic_iff_exists_orderOf_eq_natCard.

      @[deprecated isAddCyclic_iff_exists_addOrderOf_eq_natCard (since := "2024-12-20")]

      Alias of isAddCyclic_iff_exists_addOrderOf_eq_natCard.

      theorem isCyclic_of_orderOf_eq_card {α : Type u_1} [Group α] [Finite α] (x : α) (hx : orderOf x = Nat.card α) :
      theorem isAddCyclic_of_addOrderOf_eq_card {α : Type u_1} [AddGroup α] [Finite α] (x : α) (hx : addOrderOf x = Nat.card α) :
      theorem isCyclic_of_card_le_orderOf {α : Type u_1} [Group α] [Finite α] (x : α) (hx : Nat.card α orderOf x) :
      theorem isAddCyclic_of_card_le_addOrderOf {α : Type u_1} [AddGroup α] [Finite α] (x : α) (hx : Nat.card α addOrderOf x) :
      theorem zpowers_eq_top_of_prime_card {G : Type u_2} [Group G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g 1) :

      Any non-identity element of a finite group of prime order generates the group.

      theorem zmultiples_eq_top_of_prime_card {G : Type u_2} [AddGroup G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g 0) :

      Any non-identity element of a finite group of prime order generates the group.

      theorem mem_zpowers_of_prime_card {G : Type u_2} [Group G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g 1) :
      theorem mem_zmultiples_of_prime_card {G : Type u_2} [AddGroup G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g 0) :
      theorem mem_powers_of_prime_card {G : Type u_2} [Group G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g 1) :
      theorem mem_multiples_of_prime_card {G : Type u_2} [AddGroup G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g g' : G} (hg : g 0) :
      theorem powers_eq_top_of_prime_card {G : Type u_2} [Group G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g 1) :
      theorem multiples_eq_top_of_prime_card {G : Type u_2} [AddGroup G] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card G = p) {g : G} (hg : g 0) :
      theorem isCyclic_of_prime_card {α : Type u_1} [Group α] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card α = p) :

      A finite group of prime order is cyclic.

      theorem isAddCyclic_of_prime_card {α : Type u_1} [AddGroup α] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card α = p) :

      A finite group of prime order is cyclic.

      theorem isCyclic_of_card_dvd_prime {α : Type u_1} [Group α] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card α p) :

      A finite group of order dividing a prime is cyclic.

      theorem isAddCyclic_of_card_dvd_prime {α : Type u_1} [AddGroup α] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card α p) :

      A finite group of order dividing a prime is cyclic.

      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) :
      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) :
      theorem MulEquiv.isCyclic {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] (e : G ≃* G') :
      theorem AddEquiv.isAddCyclic {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] (e : G ≃+ G') :
      theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u_1} [Group α] {g : α} (hx : ∀ (x : α), x Subgroup.zpowers g) :
      theorem addOrderOf_eq_card_of_forall_mem_zmultiples {α : Type u_1} [AddGroup α] {g : α} (hx : ∀ (x : α), x AddSubgroup.zmultiples g) :
      @[deprecated orderOf_eq_card_of_forall_mem_zpowers (since := "2024-11-15")]
      theorem orderOf_generator_eq_natCard {α : Type u_1} [Group α] {g : α} (hx : ∀ (x : α), x Subgroup.zpowers g) :

      Alias of orderOf_eq_card_of_forall_mem_zpowers.

      @[deprecated addOrderOf_eq_card_of_forall_mem_zmultiples (since := "2024-11-15")]
      theorem addOrderOf_generator_eq_natCard {α : Type u_1} [AddGroup α] {g : α} (hx : ∀ (x : α), x AddSubgroup.zmultiples g) :

      Alias of addOrderOf_eq_card_of_forall_mem_zmultiples.

      theorem exists_pow_ne_one_of_isCyclic {G : Type u_2} [Group G] [G_cyclic : IsCyclic G] {k : } (k_pos : k 0) (k_lt_card_G : k < Nat.card G) :
      ∃ (a : G), a ^ k 1
      theorem exists_nsmul_ne_zero_of_isAddCyclic {G : Type u_2} [AddGroup G] [G_cyclic : IsAddCyclic G] {k : } (k_pos : k 0) (k_lt_card_G : k < Nat.card G) :
      ∃ (a : G), k a 0
      theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers {α : Type u_1} [Group α] [Infinite α] {g : α} (h : ∀ (x : α), x Subgroup.zpowers g) :
      instance Bot.isCyclic {α : Type u_1} [Group α] :
      instance Bot.isAddCyclic {α : Type u_1} [AddGroup α] :
      instance Subgroup.isCyclic {α : Type u_1} [Group α] [IsCyclic α] (H : Subgroup α) :
      instance AddSubgroup.isAddCyclic {α : Type u_1} [AddGroup α] [IsAddCyclic α] (H : AddSubgroup α) :
      theorem isCyclic_of_injective {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (hf : Function.Injective f) :
      theorem isAddCyclic_of_injective {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [IsAddCyclic G'] (f : G →+ G') (hf : Function.Injective f) :
      theorem Subgroup.isCyclic_of_le {G : Type u_2} [Group G] {H H' : Subgroup G} (h : H H') [IsCyclic H'] :
      theorem AddSubgroup.isAddCyclic_of_le {G : Type u_2} [AddGroup G] {H H' : AddSubgroup G} (h : H H') [IsAddCyclic H'] :
      theorem IsCyclic.card_pow_eq_one_le {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] [IsCyclic α] {n : } (hn0 : 0 < n) :
      {a : α | a ^ n = 1}.card n
      theorem IsAddCyclic.card_nsmul_eq_zero_le {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : } (hn0 : 0 < n) :
      {a : α | n a = 0}.card n
      theorem IsCyclic.exists_monoid_generator {α : Type u_1} [Group α] [Finite α] [IsCyclic α] :
      ∃ (x : α), ∀ (y : α), y Submonoid.powers x
      theorem IsAddCyclic.exists_addMonoid_generator {α : Type u_1} [AddGroup α] [Finite α] [IsAddCyclic α] :
      ∃ (x : α), ∀ (y : α), y AddSubmonoid.multiples x
      theorem IsCyclic.exists_ofOrder_eq_natCard {α : Type u_1} [Group α] [h : IsCyclic α] :
      ∃ (g : α), orderOf g = Nat.card α
      theorem IsAddCyclic.exists_ofOrder_eq_natCard {α : Type u_1} [AddGroup α] [h : IsAddCyclic α] :
      ∃ (g : α), addOrderOf g = Nat.card α
      noncomputable def MulDistribMulAction.toMonoidHomZModOfIsCyclic (G : Type u_2) [Group G] (M : Type u_4) [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : } (hn : Nat.card G = n) :

      A distributive action of a monoid on a finite cyclic group of order n factors through an action on ZMod n.

      Equations
      Instances For
        theorem MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply {G : Type u_2} [Group G] {M : Type u_4} [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : } (hn : Nat.card G = n) (m : M) (g : G) (k : ) (h : (toMonoidHomZModOfIsCyclic G M hn) m = k) :
        m g = g ^ k
        theorem IsCyclic.unique_zpow_zmod {α : Type u_1} {a : α} [Group α] [Fintype α] (ha : ∀ (x : α), x Subgroup.zpowers a) (x : α) :
        ∃! n : ZMod (Fintype.card α), x = a ^ n.val
        theorem IsAddCyclic.unique_zsmul_zmod {α : Type u_1} {a : α} [AddGroup α] [Fintype α] (ha : ∀ (x : α), x AddSubgroup.zmultiples a) (x : α) :
        theorem IsCyclic.image_range_orderOf {α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x Subgroup.zpowers a) :
        theorem IsAddCyclic.image_range_addOrderOf {α : Type u_1} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x AddSubgroup.zmultiples a) :
        theorem IsCyclic.image_range_card {α : Type u_1} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x Subgroup.zpowers a) :
        Finset.image (fun (i : ) => a ^ i) (Finset.range (Nat.card α)) = Finset.univ
        theorem IsAddCyclic.image_range_card {α : Type u_1} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x AddSubgroup.zmultiples a) :
        theorem IsCyclic.ext {G : Type u_2} [Group G] [Finite G] [IsCyclic G] {d : } {a b : ZMod d} (hGcard : Nat.card G = d) (h : ∀ (t : G), t ^ a.val = t ^ b.val) :
        a = b
        theorem IsAddCyclic.ext {G : Type u_2} [AddGroup G] [Finite G] [IsAddCyclic G] {d : } {a b : ZMod d} (hGcard : Nat.card G = d) (h : ∀ (t : G), a.val t = b.val t) :
        a = b
        theorem card_orderOf_eq_totient_aux₂ {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n{a : α | a ^ n = 1}.card n) {d : } (hd : d Fintype.card α) :
        {a : α | orderOf a = d}.card = d.totient
        theorem card_addOrderOf_eq_totient_aux₂ {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n{a : α | n a = 0}.card n) {d : } (hd : d Fintype.card α) :
        {a : α | addOrderOf a = d}.card = d.totient
        theorem isCyclic_of_card_pow_eq_one_le {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n{a : α | a ^ n = 1}.card n) :

        Stacks Tag 09HX (This theorem is stronger than 09HX. It removes the abelian condition, and requires only instead of =.)

        theorem isAddCyclic_of_card_nsmul_eq_zero_le {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n{a : α | n a = 0}.card n) :
        theorem IsCyclic.card_orderOf_eq_totient {α : Type u_1} [Group α] [IsCyclic α] [Fintype α] {d : } (hd : d Fintype.card α) :
        {a : α | orderOf a = d}.card = d.totient
        theorem IsAddCyclic.card_addOrderOf_eq_totient {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : } (hd : d Fintype.card α) :
        {a : α | addOrderOf a = d}.card = d.totient
        theorem isSimpleGroup_of_prime_card {α : Type u_1} [Group α] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card α = p) :

        A finite group of prime order is simple.

        theorem isSimpleAddGroup_of_prime_card {α : Type u_1} [AddGroup α] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card α = p) :

        A finite group of prime order is simple.

        theorem commutative_of_cyclic_center_quotient {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (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 commGroupOfCyclicCenterQuotient for the CommGroup instance.

        theorem commutative_of_addCyclic_center_quotient {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [IsAddCyclic G'] (f : G →+ G') (hf : f.ker AddSubgroup.center G) (a b : G) :
        a + b = b + a

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

        def commGroupOfCyclicCenterQuotient {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (hf : f.ker Subgroup.center G) :

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

        Equations
        Instances For

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

          Equations
          Instances For
            @[instance 100]
            instance IsSimpleGroup.isCyclic {α : Type u_1} [CommGroup α] [IsSimpleGroup α] :
            @[instance 100]
            @[simp]
            theorem not_isCyclic_iff_exponent_eq_prime {α : Type u_1} [Group α] {p : } (hp : Nat.Prime p) ( : Nat.card α = p ^ 2) :

            A group of order p ^ 2 is not cyclic if and only if its exponent is p.

            The kernel of zmultiplesHom G g is equal to the additive subgroup generated by addOrderOf g.

            theorem zpowersHom_ker_eq {G : Type u_2} [Group G] (g : G) :

            The kernel of zpowersHom G g is equal to the subgroup generated by orderOf g.

            noncomputable def zmodAddCyclicAddEquiv {G : Type u_2} [AddGroup G] (h : IsAddCyclic G) :

            The isomorphism from ZMod n to any cyclic additive group of Nat.card equal to n.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              noncomputable def zmodCyclicMulEquiv {G : Type u_2} [Group G] (h : IsCyclic G) :

              The isomorphism from Multiplicative (ZMod n) to any cyclic group of Nat.card equal to n.

              Equations
              Instances For
                noncomputable def addEquivOfAddCyclicCardEq {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] [hG : IsAddCyclic G] [hH : IsAddCyclic G'] (hcard : Nat.card G = Nat.card G') :
                G ≃+ G'

                Two cyclic additive groups of the same cardinality are isomorphic.

                Equations
                Instances For
                  noncomputable def mulEquivOfCyclicCardEq {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [hG : IsCyclic G] [hH : IsCyclic G'] (hcard : Nat.card G = Nat.card G') :
                  G ≃* G'

                  Two cyclic groups of the same cardinality are isomorphic.

                  Equations
                  Instances For
                    noncomputable def mulEquivOfPrimeCardEq {G : Type u_2} {G' : Type u_3} {p : } [Group G] [Group G'] [Fact (Nat.Prime p)] (hG : Nat.card G = p) (hH : Nat.card G' = p) :
                    G ≃* G'

                    Two groups of the same prime cardinality are isomorphic.

                    Equations
                    Instances For
                      noncomputable def addEquivOfPrimeCardEq {G : Type u_2} {G' : Type u_3} {p : } [AddGroup G] [AddGroup G'] [Fact (Nat.Prime p)] (hG : Nat.card G = p) (hH : Nat.card G' = p) :
                      G ≃+ G'

                      Two additive groups of the same prime cardinality are isomorphic.

                      Equations
                      Instances For
                        noncomputable def IsCyclic.mulAutMulEquiv (G : Type u_2) [Group G] [h : IsCyclic G] :

                        The automorphism group of a cyclic group is isomorphic to the multiplicative group of ZMod.

                        Equations
                        Instances For
                          @[simp]
                          theorem IsCyclic.mulAutMulEquiv_symm_apply_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : (ZMod (Nat.card G))ˣ) (a✝¹ : G) :

                          Groups with a given generator #

                          We state some results in terms of an explicitly given generator. The generating property is given as in IsCyclic.exists_generator.

                          The main statements are about the existence and uniqueness of homomorphisms and isomorphisms specified by the image of the given generator.

                          noncomputable def monoidHomOfForallMemZpowers {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' orderOf g) :
                          G →* G'

                          If g generates the group G and g' is an element of another group G' whose order divides that of g, then there is a homomorphism G →* G' mapping g to g'.

                          Equations
                          Instances For
                            noncomputable def addMonoidHomOfForallMemZmultiples {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' addOrderOf g) :
                            G →+ G'

                            If g generates the additive group G and g' is an element of another additive group G' whose order divides that of g, then there is a homomorphism G →+ G' mapping g to g'.

                            Equations
                            Instances For
                              @[simp]
                              theorem monoidHomOfForallMemZpowers_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' orderOf g) :
                              @[simp]
                              theorem addMonoidHomOfForallMemZmultiples_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' addOrderOf g) :
                              theorem MonoidHom.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) (f₁ f₂ : G →* G') :
                              f₁ = f₂ f₁ g = f₂ g

                              Two group homomorphisms G →* G' are equal if and only if they agree on a generator of G.

                              theorem AddMonoidHom.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) (f₁ f₂ : G →+ G') :
                              f₁ = f₂ f₁ g = f₂ g

                              Two homomorphisms G →+ G' of additive groups are equal if and only if they agree on a generator of G.

                              theorem MulEquiv.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) (f₁ f₂ : G ≃* G') :
                              f₁ = f₂ f₁ g = f₂ g

                              Two group isomorphisms G ≃* G' are equal if and only if they agree on a generator of G.

                              theorem AddEquiv.eq_iff_eq_on_generator {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) (f₁ f₂ : G ≃+ G') :
                              f₁ = f₂ f₁ g = f₂ g

                              Two isomorphisms G ≃+ G' of additive groups are equal if and only if they agree on a generator of G.

                              noncomputable def mulEquivOfOrderOfEq {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x Subgroup.zpowers g') (h : orderOf g = orderOf g') :
                              G ≃* G'

                              Given two groups that are generated by elements g and g' of the same order, we obtain an isomorphism sending g to g'.

                              Equations
                              Instances For
                                noncomputable def addEquivOfAddOrderOfEq {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :
                                G ≃+ G'

                                Given two additive groups that are generated by elements g and g' of the same order, we obtain an isomorphism sending g to g'.

                                Equations
                                Instances For
                                  @[simp]
                                  theorem mulEquivOfOrderOfEq_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x Subgroup.zpowers g') (h : orderOf g = orderOf g') :
                                  (mulEquivOfOrderOfEq hg hg' h) g = g'
                                  @[simp]
                                  theorem addEquivOfAddOrderOfEq_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :
                                  (addEquivOfAddOrderOfEq hg hg' h) g = g'
                                  @[simp]
                                  theorem mulEquivOfOrderOfEq_symm {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x Subgroup.zpowers g') (h : orderOf g = orderOf g') :
                                  @[simp]
                                  theorem addEquivOfAddOrderOfEq_symm {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :
                                  theorem mulEquivOfOrderOfEq_symm_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x Subgroup.zpowers g') (h : orderOf g = orderOf g') :
                                  (mulEquivOfOrderOfEq hg hg' h).symm g' = g
                                  theorem addEquivOfAddOrderOfEq_symm_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :
                                  (addEquivOfAddOrderOfEq hg hg' h).symm g' = g
                                  theorem Group.isCyclic_of_coprime_card_range_card_ker {M : Type u_4} {N : Type u_5} [CommGroup M] [Group N] (f : M →* N) (h : (Nat.card f.ker).Coprime (Nat.card f.range)) [IsCyclic f.ker] [IsCyclic f.range] :
                                  theorem Group.isCyclic_of_coprime_card_ker {M : Type u_4} {N : Type u_5} [CommGroup M] [Group N] (f : M →* N) (h : (Nat.card f.ker).Coprime (Nat.card N)) [IsCyclic f.ker] [hN : IsCyclic N] (hf : Function.Surjective f) :
                                  theorem AddGroup.isAddCyclic_of_coprime_card_ker {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddGroup N] (f : M →+ N) (h : (Nat.card f.ker).Coprime (Nat.card N)) [IsAddCyclic f.ker] [hN : IsAddCyclic N] (hf : Function.Surjective f) :
                                  theorem isCyclic_left_of_prod (M : Type u_4) (N : Type u_5) [Group M] [Group N] [cyc : IsCyclic (M × N)] :
                                  theorem isAddCyclic_left_of_prod (M : Type u_4) (N : Type u_5) [AddGroup M] [AddGroup N] [cyc : IsAddCyclic (M × N)] :
                                  theorem isCyclic_right_of_prod (M : Type u_4) (N : Type u_5) [Group M] [Group N] [cyc : IsCyclic (M × N)] :
                                  theorem isAddCyclic_right_of_prod (M : Type u_4) (N : Type u_5) [AddGroup M] [AddGroup N] [cyc : IsAddCyclic (M × N)] :
                                  theorem coprime_card_of_isCyclic_prod (M : Type u_4) (N : Type u_5) [Group M] [Group N] [cyc : IsCyclic (M × N)] [Finite M] [Finite N] :
                                  theorem coprime_card_of_isAddCyclic_prod (M : Type u_4) (N : Type u_5) [AddGroup M] [AddGroup N] [cyc : IsAddCyclic (M × N)] [Finite M] [Finite N] :
                                  theorem Group.isCyclic_prod_iff {M : Type u_4} {N : Type u_5} [Group M] [Group N] :

                                  The product of two finite groups is cyclic iff both of them are cyclic and their orders are coprime.

                                  The product of two finite additive groups is cyclic iff both of them are cyclic and their orders are coprime.