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
    class IsCyclic (α : Type u) [Group α] :

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

    Instances
      Equations
      • =
      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
      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

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

          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 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_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 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
              • =
              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_3 {α : Type u_1} [AddGroup α] (H : AddSubgroup α) (motive : (∃ x ∈ H, x 0)Prop) :
                ∀ (hx : ∃ x ∈ H, x 0), (∀ (x : α) (hx₁ : x H) (hx₂ : x 0), motive )motive hx
                Equations
                • =
                Instances For
                  abbrev AddSubgroup.isAddCyclic.match_2 {α : Type u_1} [AddGroup α] (H : AddSubgroup α) (motive : HProp) :
                  ∀ (x : H), (∀ (x : α) (hx : x H), motive { val := x, property := hx })motive x
                  Equations
                  • =
                  Instances For
                    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
                    abbrev IsAddCyclic.card_nsmul_eq_zero_le.match_2 {α : Type u_1} [Fintype α] {n : } (motive : Nat.gcd n (Fintype.card α) Fintype.card αProp) :
                    ∀ (x : Nat.gcd n (Fintype.card α) Fintype.card α), (∀ (m : ) (hm : Fintype.card α = Nat.gcd n (Fintype.card α) * m), motive )motive x
                    Equations
                    • =
                    Instances For
                      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 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 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 = ZMod.val n a
                        theorem IsCyclic.unique_zpow_zmod {α : Type u} {a : α} [Group α] [Fintype α] (ha : ∀ (x : α), x Subgroup.zpowers a) (x : α) :
                        ∃! (n : ZMod (Fintype.card α)), x = a ^ ZMod.val n
                        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), ZMod.val a t = ZMod.val b 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 ^ ZMod.val a = t ^ ZMod.val b) :
                        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 = Nat.totient d
                        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 = Nat.totient d
                        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 = Nat.totient d
                          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 = Nat.totient d
                          @[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 = Nat.totient d

                          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.

                          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 : (AddMonoidHom.range f)), ∀ (x : (AddMonoidHom.range f)), x AddSubgroup.zmultiples g)Prop) :
                          ∀ (x : ∃ (g : (AddMonoidHom.range f)), ∀ (x : (AddMonoidHom.range f)), x AddSubgroup.zmultiples g), (∀ (x : H) (y : G) (hxy : f y = x) (hx : ∀ (a : (AddMonoidHom.range f)), a AddSubgroup.zmultiples { val := x, property := }), motive )motive x
                          Equations
                          • =
                          Instances For
                            theorem commutative_of_addCyclic_center_quotient {G : Type u_1} {H : Type u_2} [AddGroup G] [AddGroup H] [IsAddCyclic H] (f : G →+ H) (hf : AddMonoidHom.ker f 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_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 : { val := f b, property := } AddSubgroup.zmultiples { val := x, property := }Prop) :
                            ∀ (x_1 : { val := f b, property := } AddSubgroup.zmultiples { val := x, property := }), (∀ (n : ) (hn : (fun (x_2 : ) => x_2 { val := x, property := }) n = { val := f b, property := }), 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 : MonoidHom.ker f 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 : AddMonoidHom.ker f 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.

                              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 : MonoidHom.ker f Subgroup.center G) :

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

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

                                    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) :
                                    MonoidHom.ker ((zpowersHom G) g) = 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