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

class IsAddCyclic (α : Type u) [AddGroup α] :

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

Instances
    theorem IsAddCyclic.exists_generator {α : Type u} [AddGroup α] [self : IsAddCyclic α] :
    ∃ (g : α), ∀ (x : α), x AddSubgroup.zmultiples g
    class IsCyclic (α : Type u) [Group α] :

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

    Instances
      theorem IsCyclic.exists_generator {α : Type u} [Group α] [self : 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
      • =
      theorem IsAddCyclic.addCommGroup.proof_1 {α : Type u_1} [hg : AddGroup α] [IsAddCyclic α] (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.

      Equations
      Instances For
        abbrev IsAddCyclic.addCommGroup.match_2 {α : Type u_1} [hg : AddGroup α] (motive : (∃ (g : α), ∀ (x : α), x AddSubgroup.zmultiples g)Prop) :
        ∀ (x : ∃ (g : α), ∀ (x : α), x AddSubgroup.zmultiples g), (∀ (w : α) (hg_1 : ∀ (x : α), x AddSubgroup.zmultiples w), motive )motive x
        Equations
        • =
        Instances For
          abbrev IsAddCyclic.addCommGroup.match_1 {α : Type u_1} [hg : AddGroup α] (y : α) :
          ∀ (w : α) (motive : y AddSubgroup.zmultiples wProp) (x : y AddSubgroup.zmultiples w), (∀ (w_1 : ) (hm : (fun (x : ) => x w) w_1 = y), motive )motive x
          Equations
          • =
          Instances For
            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
              • =
              abbrev AddSubgroup.isAddCyclic.match_1 {α : Type u_1} [AddGroup α] (g : α) (x : α) (motive : x AddSubgroup.zmultiples gProp) :
              ∀ (x_1 : x AddSubgroup.zmultiples g), (∀ (k : ) (hk : (fun (x : ) => x g) k = x), motive )motive x_1
              Equations
              • =
              Instances For
                abbrev AddSubgroup.isAddCyclic.match_2 {α : Type u_1} [AddGroup α] (H : AddSubgroup α) (motive : HProp) :
                ∀ (x : H), (∀ (x : α) (hx : x H), motive x, hx)motive x
                Equations
                • =
                Instances For
                  abbrev AddSubgroup.isAddCyclic.match_3 {α : Type u_1} [AddGroup α] (H : AddSubgroup α) (motive : (xH, x 0)Prop) :
                  ∀ (hx : xH, x 0), (∀ (x : α) (hx₁ : x H) (hx₂ : x 0), motive )motive hx
                  Equations
                  • =
                  Instances For
                    instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup α) :
                    Equations
                    • =
                    abbrev IsAddCyclic.card_nsmul_eq_zero_le.match_1 {α : Type u_1} [AddGroup α] (g : α) (x : α) (motive : x AddSubmonoid.multiples gProp) :
                    ∀ (x_1 : x AddSubmonoid.multiples g), (∀ (m : ) (hm : (fun (x : ) => x g) m = x), motive )motive x_1
                    Equations
                    • =
                    Instances For
                      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
                      abbrev IsAddCyclic.card_nsmul_eq_zero_le.match_2 {α : Type u_1} [Fintype α] {n : } (motive : n.gcd (Fintype.card α) Fintype.card αProp) :
                      ∀ (x : n.gcd (Fintype.card α) Fintype.card α), (∀ (m : ) (hm : Fintype.card α = n.gcd (Fintype.card α) * m), motive )motive x
                      Equations
                      • =
                      Instances For
                        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.image_range_addOrderOf {α : Type u} {a : α} [AddGroup α] [DecidableEq α] [Fintype α] (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 α] [DecidableEq α] [Fintype α] (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 α] [DecidableEq α] [Fintype α] (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 α] [DecidableEq α] [Fintype α] (ha : ∀ (x : α), x Subgroup.zpowers a) :
                        Finset.image (fun (i : ) => a ^ i) (Finset.range (Fintype.card α)) = Finset.univ
                        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.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) :
                        abbrev isAddCyclic_of_card_nsmul_eq_zero_le.match_1 {α : Type u_1} [AddGroup α] [Fintype α] (motive : (Finset.filter (fun (a : α) => addOrderOf a = Fintype.card α) Finset.univ).NonemptyProp) :
                        ∀ (this : (Finset.filter (fun (a : α) => addOrderOf a = Fintype.card α) Finset.univ).Nonempty), (∀ (x : α) (hx : x Finset.filter (fun (a : α) => addOrderOf a = Fintype.card α) Finset.univ), motive )motive this
                        Equations
                        • =
                        Instances For
                          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 addCommGroup_of_cycle_center_quotient for the AddCommGroup instance.

                          abbrev commutative_of_addCyclic_center_quotient.match_2 {G : Type u_2} {H : Type u_1} [AddGroup G] [AddGroup H] (f : G →+ H) (motive : (∃ (g : f.range), ∀ (x : f.range), x AddSubgroup.zmultiples g)Prop) :
                          ∀ (x : ∃ (g : f.range), ∀ (x : f.range), x AddSubgroup.zmultiples g), (∀ (x : H) (y : G) (hxy : f y = x) (hx : ∀ (a : f.range), a AddSubgroup.zmultiples x, ), motive )motive x
                          Equations
                          • =
                          Instances For
                            abbrev commutative_of_addCyclic_center_quotient.match_1 {G : Type u_2} {H : Type u_1} [AddGroup G] [AddGroup H] (f : G →+ H) (b : G) (x : H) (y : G) (hxy : f y = x) (motive : f b, AddSubgroup.zmultiples x, Prop) :
                            ∀ (x_1 : f b, AddSubgroup.zmultiples x, ), (∀ (n : ) (hn : (fun (x_2 : ) => x_2 x, ) n = f b, ), motive )motive x_1
                            Equations
                            • =
                            Instances For
                              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 commGroup_of_cycle_center_quotient 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 addCommGroup_of_cycle_center_quotient for the AddCommGroup instance.

                              def commutativeOfAddCycleCenterQuotient {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 commGroupOfCycleCenterQuotient {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
                                  • =
                                  abbrev IsAddCyclic.of_exponent_eq_card.match_1 {α : Type u_1} [AddCommGroup α] [Fintype α] (motive : (aFinset.univ, addOrderOf a = (Finset.image addOrderOf Finset.univ).max' )Prop) :
                                  ∀ (x : aFinset.univ, addOrderOf a = (Finset.image addOrderOf Finset.univ).max' ), (∀ (g : α) (left : g Finset.univ) (hg : addOrderOf g = (Finset.image addOrderOf Finset.univ).max' ), motive )motive x
                                  Equations
                                  • =
                                  Instances For
                                    @[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.

                                                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
                                                  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_1 {G : Type u_1} [AddGroup G] {g : G} (hg : ∀ (x : G), x AddSubgroup.zmultiples g) (x : G) :
                                                  ∃ (k : ), k g = x
                                                  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) :
                                                  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_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') :
                                                    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_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 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_2 {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {g : G} {g' : 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