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 IsAddCyclic.exists_generator {α : Type u} [AddGroup α] [IsAddCyclic α] :
∃ (g : α), ∀ (x : α), x AddSubgroup.zmultiples g
theorem IsCyclic.exists_generator {α : Type u} [Group α] [IsCyclic α] :
∃ (g : α), ∀ (x : α), x Subgroup.zpowers g
@[instance 100]
Equations
  • =
@[instance 100]
instance isCyclic_of_subsingleton {α : Type u} [Group α] [Subsingleton α] :
Equations
  • =
Equations
  • =
instance isAddCyclic_additive {α : Type u} [Group α] [IsCyclic α] :
Equations
  • =

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

Equations
Instances For
    theorem IsAddCyclic.addCommGroup.proof_1 {α : Type u_1} [hg : AddGroup α] [IsAddCyclic α] (x : α) (y : α) :
    x + y = y + x
    def IsCyclic.commGroup {α : Type u} [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 non-cyclic additive group is non-trivial.

      theorem Nontrivial.of_not_isCyclic {α : Type u} [Group α] (nc : ¬IsCyclic α) :

      A non-cyclic multiplicative group is non-trivial.

      theorem AddMonoidHom.map_addCyclic {G : Type u_1} [AddGroup G] [h : IsAddCyclic G] (σ : G →+ G) :
      ∃ (m : ), ∀ (g : G), σ g = m g
      theorem MonoidHom.map_cyclic {G : Type u_1} [Group G] [h : IsCyclic G] (σ : G →* G) :
      ∃ (m : ), ∀ (g : G), σ g = g ^ m
      @[deprecated AddMonoidHom.map_addCyclic]
      theorem MonoidAddHom.map_add_cyclic {G : Type u_1} [AddGroup G] [h : IsAddCyclic G] (σ : G →+ G) :
      ∃ (m : ), ∀ (g : G), σ g = m g

      Alias of AddMonoidHom.map_addCyclic.

      theorem isCyclic_of_orderOf_eq_card {α : Type u} [Group α] [Fintype α] (x : α) (hx : orderOf x = Fintype.card α) :
      @[deprecated isAddCyclic_of_addOrderOf_eq_card]
      theorem isAddCyclic_of_orderOf_eq_card {α : Type u} [AddGroup α] [Fintype α] (x : α) (hx : addOrderOf x = Fintype.card α) :

      Alias of isAddCyclic_of_addOrderOf_eq_card.

      theorem Subgroup.eq_bot_or_eq_top_of_prime_card {G : Type u_1} [Group G] :
      ∀ {x : Fintype G} (H : Subgroup G) [hp : Fact (Nat.Prime (Fintype.card G))], H = H =
      theorem zmultiples_eq_top_of_prime_card {G : Type u_1} [AddGroup G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g : G}, g 0AddSubgroup.zmultiples g =

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

      theorem zpowers_eq_top_of_prime_card {G : Type u_1} [Group G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g : G}, g 1Subgroup.zpowers g =

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

      theorem mem_zmultiples_of_prime_card {G : Type u_1} [AddGroup G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g g' : G}, g 0g' AddSubgroup.zmultiples g
      theorem mem_zpowers_of_prime_card {G : Type u_1} [Group G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g g' : G}, g 1g' Subgroup.zpowers g
      theorem mem_multiples_of_prime_card {G : Type u_1} [AddGroup G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g g' : G}, g 0g' AddSubmonoid.multiples g
      theorem mem_powers_of_prime_card {G : Type u_1} [Group G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g g' : G}, g 1g' Submonoid.powers g
      theorem multiples_eq_top_of_prime_card {G : Type u_1} [AddGroup G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g : G}, g 0AddSubmonoid.multiples g =
      theorem powers_eq_top_of_prime_card {G : Type u_1} [Group G] :
      ∀ {x : Fintype G} {p : } [hp : Fact (Nat.Prime p)], Fintype.card G = p∀ {g : G}, g 1Submonoid.powers g =
      theorem isAddCyclic_of_prime_card {α : Type u} [AddGroup α] [Fintype α] {p : } [hp : Fact (Nat.Prime p)] (h : Fintype.card α = p) :

      A finite group of prime order is cyclic.

      theorem isCyclic_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 isAddCyclic_of_card_dvd_prime {α : Type u} [AddGroup α] {p : } [hp : Fact (Nat.Prime p)] (h : Nat.card α p) :

      A finite group of order dividing a prime is cyclic.

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

      A finite group of order dividing a prime is cyclic.

      theorem isAddCyclic_of_surjective {H : Type u_1} {G : Type u_2} {F : Type u_3} [AddGroup H] [AddGroup G] [hH : IsAddCyclic H] [FunLike F H G] [AddMonoidHomClass F H G] (f : F) (hf : Function.Surjective f) :
      theorem isCyclic_of_surjective {H : Type u_1} {G : Type u_2} {F : Type u_3} [Group H] [Group G] [hH : IsCyclic H] [FunLike F H G] [MonoidHomClass F H G] (f : F) (hf : Function.Surjective f) :
      theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u} [Group α] [Fintype α] {g : α} (hx : ∀ (x : α), x Subgroup.zpowers g) :
      theorem addOrderOf_generator_eq_natCard {α : Type u} {a : α} [AddGroup α] (h : ∀ (x : α), x AddSubgroup.zmultiples a) :
      theorem orderOf_generator_eq_natCard {α : Type u} {a : α} [Group α] (h : ∀ (x : α), x Subgroup.zpowers a) :
      theorem exists_nsmul_ne_zero_of_isAddCyclic {G : Type u_1} [AddGroup G] [Fintype G] [G_cyclic : IsAddCyclic G] {k : } (k_pos : k 0) (k_lt_card_G : k < Fintype.card G) :
      ∃ (a : G), k a 0
      theorem exists_pow_ne_one_of_isCyclic {G : Type u_1} [Group G] [Fintype G] [G_cyclic : IsCyclic G] {k : } (k_pos : k 0) (k_lt_card_G : k < Fintype.card G) :
      ∃ (a : G), a ^ k 1
      theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers {α : Type u} [Group α] [Infinite α] {g : α} (h : ∀ (x : α), x Subgroup.zpowers g) :
      instance Bot.isAddCyclic {α : Type u} [AddGroup α] :
      Equations
      • =
      instance Bot.isCyclic {α : Type u} [Group α] :
      Equations
      • =
      instance AddSubgroup.isAddCyclic {α : Type u} [AddGroup α] [IsAddCyclic α] (H : AddSubgroup α) :
      Equations
      • =
      instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup α) :
      Equations
      • =
      theorem IsAddCyclic.card_nsmul_eq_zero_le {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : } (hn0 : 0 < n) :
      (Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n
      theorem IsCyclic.card_pow_eq_one_le {α : Type u} [Group α] [DecidableEq α] [Fintype α] [IsCyclic α] {n : } (hn0 : 0 < n) :
      (Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card n
      @[deprecated IsAddCyclic.card_nsmul_eq_zero_le]
      theorem IsAddCyclic.card_pow_eq_one_le {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : } (hn0 : 0 < n) :
      (Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n

      Alias of IsAddCyclic.card_nsmul_eq_zero_le.

      theorem IsAddCyclic.exists_addMonoid_generator {α : Type u} [AddGroup α] [Finite α] [IsAddCyclic α] :
      ∃ (x : α), ∀ (y : α), y AddSubmonoid.multiples x
      theorem IsCyclic.exists_monoid_generator {α : Type u} [Group α] [Finite α] [IsCyclic α] :
      ∃ (x : α), ∀ (y : α), y Submonoid.powers x
      theorem IsAddCyclic.exists_ofOrder_eq_natCard {α : Type u} [AddGroup α] [h : IsAddCyclic α] :
      ∃ (g : α), addOrderOf g = Nat.card α
      theorem IsCyclic.exists_ofOrder_eq_natCard {α : Type u} [Group α] [h : IsCyclic α] :
      ∃ (g : α), orderOf g = Nat.card α
      theorem isCyclic_iff_exists_ofOrder_eq_natCard {α : Type u} [Group α] [Finite α] :
      IsCyclic α ∃ (g : α), orderOf g = Nat.card α
      theorem IsAddCyclic.unique_zsmul_zmod {α : Type u} {a : α} [AddGroup α] [Fintype α] (ha : ∀ (x : α), x AddSubgroup.zmultiples a) (x : α) :
      ∃! n : ZMod (Fintype.card α), x = n.val a
      theorem IsCyclic.unique_zpow_zmod {α : Type u} {a : α} [Group α] [Fintype α] (ha : ∀ (x : α), x Subgroup.zpowers a) (x : α) :
      ∃! n : ZMod (Fintype.card α), x = a ^ n.val
      theorem IsAddCyclic.image_range_addOrderOf {α : Type u} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x AddSubgroup.zmultiples a) :
      Finset.image (fun (i : ) => i a) (Finset.range (addOrderOf a)) = Finset.univ
      theorem IsCyclic.image_range_orderOf {α : Type u} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x Subgroup.zpowers a) :
      Finset.image (fun (i : ) => a ^ i) (Finset.range (orderOf a)) = Finset.univ
      theorem IsAddCyclic.image_range_card {α : Type u} {a : α} [AddGroup α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x AddSubgroup.zmultiples a) :
      Finset.image (fun (i : ) => i a) (Finset.range (Fintype.card α)) = Finset.univ
      theorem IsCyclic.image_range_card {α : Type u} {a : α} [Group α] [Fintype α] [DecidableEq α] (ha : ∀ (x : α), x Subgroup.zpowers a) :
      Finset.image (fun (i : ) => a ^ i) (Finset.range (Fintype.card α)) = Finset.univ
      theorem IsAddCyclic.ext {G : Type u_1} [AddGroup G] [Fintype G] [IsAddCyclic G] {d : } {a : ZMod d} {b : ZMod d} (hGcard : Fintype.card G = d) (h : ∀ (t : G), a.val t = b.val t) :
      a = b
      theorem IsCyclic.ext {G : Type u_1} [Group G] [Fintype G] [IsCyclic G] {d : } {a : ZMod d} {b : ZMod d} (hGcard : Fintype.card G = d) (h : ∀ (t : G), t ^ a.val = t ^ b.val) :
      a = b
      theorem card_addOrderOf_eq_totient_aux₂ {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n) {d : } (hd : d Fintype.card α) :
      (Finset.filter (fun (a : α) => addOrderOf a = d) Finset.univ).card = d.totient
      theorem card_orderOf_eq_totient_aux₂ {α : Type u} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card n) {d : } (hd : d Fintype.card α) :
      (Finset.filter (fun (a : α) => orderOf a = d) Finset.univ).card = d.totient
      theorem isAddCyclic_of_card_nsmul_eq_zero_le {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n) :
      theorem isCyclic_of_card_pow_eq_one_le {α : Type u} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card n) :
      @[deprecated isAddCyclic_of_card_nsmul_eq_zero_le]
      theorem isAddCyclic_of_card_pow_eq_one_le {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n) :

      Alias of isAddCyclic_of_card_nsmul_eq_zero_le.

      theorem IsAddCyclic.card_addOrderOf_eq_totient {α : Type u} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : } (hd : d Fintype.card α) :
      (Finset.filter (fun (a : α) => addOrderOf a = d) Finset.univ).card = d.totient
      theorem IsCyclic.card_orderOf_eq_totient {α : Type u} [Group α] [IsCyclic α] [Fintype α] {d : } (hd : d Fintype.card α) :
      (Finset.filter (fun (a : α) => orderOf a = d) Finset.univ).card = d.totient
      @[deprecated IsAddCyclic.card_addOrderOf_eq_totient]
      theorem IsAddCyclic.card_orderOf_eq_totient {α : Type u} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : } (hd : d Fintype.card α) :
      (Finset.filter (fun (a : α) => addOrderOf a = d) Finset.univ).card = d.totient

      Alias of IsAddCyclic.card_addOrderOf_eq_totient.

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

      A finite group of prime order is simple.

      theorem isSimpleGroup_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_addCyclic_center_quotient {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [IsAddCyclic H] (f : G →+ H) (hf : f.ker AddSubgroup.center G) (a : G) (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.

      theorem commutative_of_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [Group G] [Group H] [IsCyclic H] (f : G →* H) (hf : f.ker Subgroup.center G) (a : G) (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.

      @[deprecated commutative_of_addCyclic_center_quotient]
      theorem commutative_of_add_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [IsAddCyclic H] (f : G →+ H) (hf : f.ker AddSubgroup.center G) (a : G) (b : G) :
      a + b = b + a

      Alias of commutative_of_addCyclic_center_quotient.


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

      def addCommGroupOfAddCyclicCenterQuotient {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [IsAddCyclic H] (f : G →+ H) (hf : f.ker AddSubgroup.center G) :

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

      Equations
      Instances For
        def commGroupOfCyclicCenterQuotient {G : Type u_1} {H : Type u_2} [Group G] [Group H] [IsCyclic H] (f : G →* H) (hf : f.ker Subgroup.center G) :

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

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

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

          theorem zmultiplesHom_ker_eq {G : Type u_1} [AddGroup G] (g : G) :

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

          theorem zpowersHom_ker_eq {G : Type u_1} [Group G] (g : G) :
          ((zpowersHom G) g).ker = Subgroup.zpowers (Multiplicative.ofAdd (orderOf g))

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

          noncomputable def zmodAddCyclicAddEquiv {G : Type u_1} [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_1} [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_1} {H : Type u_2} [AddGroup G] [AddGroup H] [hG : IsAddCyclic G] [hH : IsAddCyclic H] (hcard : Nat.card G = Nat.card H) :
              G ≃+ H

              Two cyclic additive groups of the same cardinality are isomorphic.

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

                Two cyclic groups of the same cardinality are isomorphic.

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

                  Two additive groups of the same prime cardinality are isomorphic.

                  Equations
                  Instances For
                    theorem addEquivOfPrimeCardEq.proof_1 {G : Type u_1} {H : Type u_2} {p : } [Fintype G] [Fintype H] (hG : Fintype.card G = p) (hH : Fintype.card H = p) :
                    noncomputable def mulEquivOfPrimeCardEq {G : Type u_1} {H : Type u_2} {p : } [Fintype G] [Fintype H] [Group G] [Group H] [Fact (Nat.Prime p)] (hG : Fintype.card G = p) (hH : Fintype.card H = p) :
                    G ≃* H

                    Two groups of the same prime cardinality are isomorphic.

                    Equations
                    Instances For

                      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.

                      theorem addMonoidHomOfForallMemZmultiples.proof_3 {G : Type u_2} {G' : Type u_1} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' addOrderOf g) (x : G) (y : G) :
                      { toFun := fun (x : G) => Classical.choose g', map_zero' := }.toFun (x + y) = { toFun := fun (x : G) => Classical.choose g', map_zero' := }.toFun x + { toFun := fun (x : G) => Classical.choose g', map_zero' := }.toFun y
                      theorem addMonoidHomOfForallMemZmultiples.proof_2 {G : Type u_2} {G' : Type u_1} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' addOrderOf g) :
                      theorem addMonoidHomOfForallMemZmultiples.proof_1 {G : Type u_1} [AddGroup G] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) (x : G) :
                      ∃ (k : ), k g = x
                      noncomputable def addMonoidHomOfForallMemZmultiples {G : Type u_1} {G' : Type u_2} [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
                        noncomputable def monoidHomOfForallMemZpowers {G : Type u_1} {G' : Type u_2} [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
                          @[simp]
                          theorem addMonoidHomOfForallMemZmultiples_apply_gen {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' addOrderOf g) :
                          @[simp]
                          theorem monoidHomOfForallMemZpowers_apply_gen {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' orderOf g) :
                          theorem AddMonoidHom.eq_iff_eq_on_generator {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) (f₁ : G →+ G') (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 MonoidHom.eq_iff_eq_on_generator {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) (f₁ : G →* G') (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 AddEquiv.eq_iff_eq_on_generator {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) (f₁ : G ≃+ G') (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.

                          theorem MulEquiv.eq_iff_eq_on_generator {G : Type u_1} {G' : Type u_2} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x Subgroup.zpowers g) (f₁ : G ≃* G') (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 addEquivOfAddOrderOfEq.proof_2 {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {g : G} {g' : G'} (h : addOrderOf g = addOrderOf g') :
                          theorem addEquivOfAddOrderOfEq.proof_1 {G : Type u_2} {G' : Type u_1} [AddGroup G] [AddGroup G'] {g : G} {g' : G'} (h : addOrderOf g = addOrderOf g') :
                          theorem addEquivOfAddOrderOfEq.proof_3 {G : Type u_1} {G' : Type u_2} [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') :
                          noncomputable def addEquivOfAddOrderOfEq {G : Type u_1} {G' : Type u_2} [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
                            theorem addEquivOfAddOrderOfEq.proof_4 {G : Type u_2} {G' : Type u_1} [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') :
                            noncomputable def mulEquivOfOrderOfEq {G : Type u_1} {G' : Type u_2} [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
                              @[simp]
                              theorem addEquivOfAddOrderOfEq_apply_gen {G : Type u_1} {G' : Type u_2} [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_apply_gen {G : Type u_1} {G' : Type u_2} [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_symm {G : Type u_1} {G' : Type u_2} [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') :
                              @[simp]
                              theorem mulEquivOfOrderOfEq_symm {G : Type u_1} {G' : Type u_2} [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 = mulEquivOfOrderOfEq hg' hg
                              theorem addEquivOfAddOrderOfEq_symm_apply_gen {G : Type u_1} {G' : Type u_2} [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 mulEquivOfOrderOfEq_symm_apply_gen {G : Type u_1} {G' : Type u_2} [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