# 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 #

• IsCyclic is a predicate on a group stating that the group is cyclic.

## Main statements #

• isCyclic_of_prime_card proves that a finite group of prime order is cyclic.
• isSimpleGroup_of_prime_card, IsSimpleGroup.isCyclic, and IsSimpleGroup.prime_card classify finite simple abelian groups.
• IsCyclic.exponent_eq_card: For a finite cyclic group G, the exponent is equal to the group's cardinality.
• IsCyclic.exponent_eq_zero_of_infinite: Infinite cyclic groups have exponent zero.
• IsCyclic.iff_exponent_eq_card: A finite commutative group is cyclic iff its exponent is equal to its cardinality.

## Tags #

cyclic group

class IsAddCyclic (α : Type u) [] :

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

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

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

• exists_generator : ∃ (g : α), ∀ (x : α),
Instances
theorem IsCyclic.exists_generator {α : Type u} [] [self : ] :
∃ (g : α), ∀ (x : α),
@[instance 100]
instance isAddCyclic_of_subsingleton {α : Type u} [] [] :
Equations
• =
@[instance 100]
instance isCyclic_of_subsingleton {α : Type u} [] [] :
Equations
• =
@[simp]
theorem isCyclic_multiplicative_iff {α : Type u} [] :
instance isCyclic_multiplicative {α : Type u} [] [] :
Equations
• =
@[simp]
Equations
• =
theorem IsAddCyclic.addCommGroup.proof_1 {α : Type u_1} [hg : ] [] (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 : ] (motive : (∃ (g : α), ∀ (x : α), )Prop) :
∀ (x : ∃ (g : α), ∀ (x : α), ), (∀ (w : α) (hg_1 : ∀ (x : α), ), motive )motive x
Equations
• =
Instances For
abbrev IsAddCyclic.addCommGroup.match_1 {α : Type u_1} [hg : ] (y : α) :
∀ (w : α) (motive : ) (x : ), (∀ (w_1 : ) (hm : (fun (x : ) => x w) w_1 = y), motive )motive x
Equations
• =
Instances For
def IsCyclic.commGroup {α : Type u} [hg : ] [] :

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

Equations
• IsCyclic.commGroup =
Instances For
theorem Nontrivial.of_not_isAddCyclic {α : Type u} [] (nc : ) :

A non-cyclic additive group is non-trivial.

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

A non-cyclic multiplicative group is non-trivial.

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

Alias of AddMonoidHom.map_addCyclic.

theorem isAddCyclic_of_addOrderOf_eq_card {α : Type u} [] [] (x : α) (hx : ) :
theorem isCyclic_of_orderOf_eq_card {α : Type u} [] [] (x : α) (hx : ) :
theorem isAddCyclic_of_orderOf_eq_card {α : Type u} [] [] (x : α) (hx : ) :

Alias of isAddCyclic_of_addOrderOf_eq_card.

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

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} [] :
∀ {x : } {p : } [hp : Fact p.Prime], ∀ {g : G}, g 1

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

theorem mem_zmultiples_of_prime_card {G : Type u_1} [] :
∀ {x : } {p : } [hp : Fact p.Prime], ∀ {g g' : G}, g 0
theorem mem_zpowers_of_prime_card {G : Type u_1} [] :
∀ {x : } {p : } [hp : Fact p.Prime], ∀ {g g' : G}, g 1
theorem mem_multiples_of_prime_card {G : Type u_1} [] :
∀ {x : } {p : } [hp : Fact p.Prime], ∀ {g g' : G}, g 0
theorem mem_powers_of_prime_card {G : Type u_1} [] :
∀ {x : } {p : } [hp : Fact p.Prime], ∀ {g g' : G}, g 1
theorem multiples_eq_top_of_prime_card {G : Type u_1} [] :
∀ {x : } {p : } [hp : Fact p.Prime], ∀ {g : G}, g 0
theorem powers_eq_top_of_prime_card {G : Type u_1} [] :
∀ {x : } {p : } [hp : Fact p.Prime], ∀ {g : G}, g 1
theorem isAddCyclic_of_prime_card {α : Type u} [] [] {p : } [hp : Fact p.Prime] (h : ) :

A finite group of prime order is cyclic.

theorem isCyclic_of_prime_card {α : Type u} [] [] {p : } [hp : Fact p.Prime] (h : ) :

A finite group of prime order is cyclic.

theorem isAddCyclic_of_surjective {H : Type u_1} {G : Type u_2} {F : Type u_3} [] [] [hH : ] [FunLike F H G] [] (f : F) (hf : ) :
theorem isCyclic_of_surjective {H : Type u_1} {G : Type u_2} {F : Type u_3} [] [] [hH : ] [FunLike F H G] [] (f : F) (hf : ) :
theorem addOrderOf_eq_card_of_forall_mem_zmultiples {α : Type u} [] [] {g : α} (hx : ∀ (x : α), ) :
theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u} [] [] {g : α} (hx : ∀ (x : α), ) :
theorem addOrderOf_generator_eq_natCard {α : Type u} {a : α} [] (h : ∀ (x : α), ) :
theorem orderOf_generator_eq_natCard {α : Type u} {a : α} [] (h : ∀ (x : α), ) :
=
theorem exists_nsmul_ne_zero_of_isAddCyclic {G : Type u_1} [] [] [G_cyclic : ] {k : } (k_pos : k 0) (k_lt_card_G : ) :
∃ (a : G), k a 0
theorem exists_pow_ne_one_of_isCyclic {G : Type u_1} [] [] [G_cyclic : ] {k : } (k_pos : k 0) (k_lt_card_G : ) :
∃ (a : G), a ^ k 1
theorem Infinite.addOrderOf_eq_zero_of_forall_mem_zmultiples {α : Type u} [] [] {g : α} (h : ∀ (x : α), ) :
= 0
theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers {α : Type u} [] [] {g : α} (h : ∀ (x : α), ) :
= 0
instance Bot.isAddCyclic {α : Type u} [] :
Equations
• =
instance Bot.isCyclic {α : Type u} [] :
Equations
• =
instance AddSubgroup.isAddCyclic {α : Type u} [] [] (H : ) :
Equations
• =
abbrev AddSubgroup.isAddCyclic.match_2 {α : Type u_1} [] (H : ) (motive : HProp) :
∀ (x : H), (∀ (x : α) (hx : x H), motive x, hx)motive x
Equations
• =
Instances For
abbrev AddSubgroup.isAddCyclic.match_3 {α : Type u_1} [] (H : ) (motive : (xH, x 0)Prop) :
∀ (hx : xH, x 0), (∀ (x : α) (hx₁ : x H) (hx₂ : x 0), motive )motive hx
Equations
• =
Instances For
abbrev AddSubgroup.isAddCyclic.match_1 {α : Type u_1} [] (g : α) (x : α) (motive : ) :
∀ (x_1 : ), (∀ (k : ) (hk : (fun (x : ) => x g) k = x), motive )motive x_1
Equations
• =
Instances For
instance Subgroup.isCyclic {α : Type u} [] [] (H : ) :
Equations
• =
abbrev IsAddCyclic.card_nsmul_eq_zero_le.match_2 {α : Type u_1} [] {n : } (motive : n.gcd () Prop) :
∀ (x : n.gcd () ), (∀ (m : ) (hm : = n.gcd () * m), motive )motive x
Equations
• =
Instances For
abbrev IsAddCyclic.card_nsmul_eq_zero_le.match_1 {α : Type u_1} [] (g : α) (x : α) (motive : ) :
∀ (x_1 : ), (∀ (m : ) (hm : (fun (x : ) => x g) m = x), motive )motive x_1
Equations
• =
Instances For
theorem IsAddCyclic.card_nsmul_eq_zero_le {α : Type u} [] [] [] [] {n : } (hn0 : 0 < n) :
(Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n
theorem IsCyclic.card_pow_eq_one_le {α : Type u} [] [] [] [] {n : } (hn0 : 0 < n) :
(Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card n
theorem IsAddCyclic.card_pow_eq_one_le {α : Type u} [] [] [] [] {n : } (hn0 : 0 < n) :
(Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n

Alias of IsAddCyclic.card_nsmul_eq_zero_le.

∃ (x : α), ∀ (y : α),
theorem IsCyclic.exists_monoid_generator {α : Type u} [] [] [] :
∃ (x : α), ∀ (y : α),
theorem IsAddCyclic.exists_ofOrder_eq_natCard {α : Type u} [] [h : ] :
∃ (g : α),
theorem IsCyclic.exists_ofOrder_eq_natCard {α : Type u} [] [h : ] :
∃ (g : α), =
theorem isAddCyclic_iff_exists_ofOrder_eq_natCard {α : Type u} [] [] :
∃ (g : α),
theorem isCyclic_iff_exists_ofOrder_eq_natCard {α : Type u} [] [] :
∃ (g : α), =
@[deprecated]
theorem IsCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype {α : Type u} [] [] :
∃ (g : α), =

Alias of isCyclic_iff_exists_ofOrder_eq_natCard.

@[deprecated]
theorem IsAddCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype {α : Type u} [] [] :
∃ (g : α),
theorem IsAddCyclic.image_range_addOrderOf {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun (i : ) => i a) () = Finset.univ
theorem IsCyclic.image_range_orderOf {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun (i : ) => a ^ i) () = Finset.univ
theorem IsAddCyclic.image_range_card {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun (i : ) => i a) () = Finset.univ
theorem IsCyclic.image_range_card {α : Type u} {a : α} [] [] [] (ha : ∀ (x : α), ) :
Finset.image (fun (i : ) => a ^ i) () = Finset.univ
theorem IsAddCyclic.unique_zsmul_zmod {α : Type u} {a : α} [] [] (ha : ∀ (x : α), ) (x : α) :
∃! n : ZMod (), x = n.val a
theorem IsCyclic.unique_zpow_zmod {α : Type u} {a : α} [] [] (ha : ∀ (x : α), ) (x : α) :
∃! n : ZMod (), x = a ^ n.val
theorem IsAddCyclic.ext {G : Type u_1} [] [] [] {d : } {a : ZMod d} {b : ZMod d} (hGcard : ) (h : ∀ (t : G), a.val t = b.val t) :
a = b
theorem IsCyclic.ext {G : Type u_1} [] [] [] {d : } {a : ZMod d} {b : ZMod d} (hGcard : ) (h : ∀ (t : G), t ^ a.val = t ^ b.val) :
a = b
theorem card_addOrderOf_eq_totient_aux₂ {α : Type u} [] [] [] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => n a = 0) Finset.univ).card n) {d : } (hd : ) :
(Finset.filter (fun (a : α) => = d) Finset.univ).card = d.totient
theorem card_orderOf_eq_totient_aux₂ {α : Type u} [] [] [] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card n) {d : } (hd : ) :
(Finset.filter (fun (a : α) => = d) Finset.univ).card = d.totient
theorem isAddCyclic_of_card_nsmul_eq_zero_le {α : Type u} [] [] [] (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} [] [] (motive : (Finset.filter (fun (a : α) => ) Finset.univ).NonemptyProp) :
∀ (this : (Finset.filter (fun (a : α) => ) Finset.univ).Nonempty), (∀ (x : α) (hx : x Finset.filter (fun (a : α) => ) Finset.univ), motive )motive this
Equations
• =
Instances For
theorem isCyclic_of_card_pow_eq_one_le {α : Type u} [] [] [] (hn : ∀ (n : ), 0 < n(Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card n) :
theorem isAddCyclic_of_card_pow_eq_one_le {α : Type u} [] [] [] (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} [] [] [] {d : } (hd : ) :
(Finset.filter (fun (a : α) => = d) Finset.univ).card = d.totient
theorem IsCyclic.card_orderOf_eq_totient {α : Type u} [] [] [] {d : } (hd : ) :
(Finset.filter (fun (a : α) => = d) Finset.univ).card = d.totient
theorem IsAddCyclic.card_orderOf_eq_totient {α : Type u} [] [] [] {d : } (hd : ) :
(Finset.filter (fun (a : α) => = d) Finset.univ).card = d.totient

Alias of IsAddCyclic.card_addOrderOf_eq_totient.

theorem isSimpleAddGroup_of_prime_card {α : Type u} [] [] {p : } [hp : Fact p.Prime] (h : ) :

A finite group of prime order is simple.

theorem isSimpleGroup_of_prime_card {α : Type u} [] [] {p : } [hp : Fact p.Prime] (h : ) :

A finite group of prime order is simple.

theorem commutative_of_addCyclic_center_quotient {G : Type u_1} {H : Type u_2} [] [] [] (f : G →+ H) (hf : f.ker ) (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} [] [] (f : G →+ H) (motive : (∃ (g : f.range), ∀ (x : f.range), )Prop) :
∀ (x : ∃ (g : f.range), ∀ (x : f.range), ), (∀ (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} [] [] (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} [] [] [] (f : G →* H) (hf : f.ker ) (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.

theorem commutative_of_add_cyclic_center_quotient {G : Type u_1} {H : Type u_2} [] [] [] (f : G →+ H) (hf : f.ker ) (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} [] [] [] (f : G →+ H) (hf : f.ker ) :

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

Equations
• = let __src := let_fun this := inferInstance; this;
Instances For
def commGroupOfCycleCenterQuotient {G : Type u_1} {H : Type u_2} [] [] [] (f : G →* H) (hf : f.ker ) :

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

Equations
• = let __src := let_fun this := inferInstance; this;
Instances For
@[instance 100]
Equations
• =
@[instance 100]
instance IsSimpleGroup.isCyclic {α : Type u} [] [] :
Equations
• =
theorem IsSimpleAddGroup.prime_card {α : Type u} [] [] [] :
().Prime
theorem IsSimpleGroup.prime_card {α : Type u} [] [] [] :
().Prime
Equations
Equations
• =
instance ZMod.instIsSimpleAddGroup {p : } [Fact p.Prime] :
Equations
• =
theorem IsAddCyclic.exponent_eq_card {α : Type u} [] [] [] :
theorem IsCyclic.exponent_eq_card {α : Type u} [] [] [] :
abbrev IsAddCyclic.of_exponent_eq_card.match_1 {α : Type u_1} [] [] (motive : (aFinset.univ, = (Finset.image (fun (g : α) => ) Finset.univ).max' )Prop) :
∀ (x : aFinset.univ, = (Finset.image (fun (g : α) => ) Finset.univ).max' ), (∀ (g : α) (left : g Finset.univ) (hg : = (Finset.image (fun (g : α) => ) Finset.univ).max' ), motive )motive x
Equations
• =
Instances For
theorem IsAddCyclic.of_exponent_eq_card {α : Type u} [] [] (h : ) :
theorem IsCyclic.of_exponent_eq_card {α : Type u} [] [] (h : ) :
theorem IsCyclic.iff_exponent_eq_card {α : Type u} [] [] :
@[simp]
theorem ZMod.exponent (n : ) :
= n
theorem not_isAddCyclic_iff_exponent_eq_prime {α : Type u} [] {p : } (hp : p.Prime) (hα : = p ^ 2) :
theorem not_isCyclic_iff_exponent_eq_prime {α : Type u} [] {p : } (hp : p.Prime) (hα : = 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} [] (g : G) :
(() g).ker =

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

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

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

noncomputable def zmodAddCyclicAddEquiv {G : Type u_1} [] (h : ) :
ZMod () ≃+ 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} [] (h : ) :

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} [] [] [hG : ] [hH : ] (hcard : ) :
G ≃+ H

Two cyclic additive groups of the same cardinality are isomorphic.

Equations
• = (hcard).symm.trans
Instances For
noncomputable def mulEquivOfCyclicCardEq {G : Type u_1} {H : Type u_2} [] [] [hG : ] [hH : ] (hcard : ) :
G ≃* H

Two cyclic groups of the same cardinality are isomorphic.

Equations
• = (hcard).symm.trans ()
Instances For
noncomputable def addEquivOfPrimeCardEq {G : Type u_1} {H : Type u_2} {p : } [] [] [] [] [Fact p.Prime] (hG : ) (hH : ) :
G ≃+ H

Two additive groups of the same prime cardinality are isomorphic.

Equations
• = let_fun hGcyc := ; let_fun hHcyc := ;
Instances For
theorem addEquivOfPrimeCardEq.proof_1 {G : Type u_1} {H : Type u_2} {p : } [] [] (hG : ) (hH : ) :
noncomputable def mulEquivOfPrimeCardEq {G : Type u_1} {H : Type u_2} {p : } [] [] [] [] [Fact p.Prime] (hG : ) (hH : ) :
G ≃* H

Two groups of the same prime cardinality are isomorphic.

Equations
• = let_fun hGcyc := ; let_fun hHcyc := ;
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_2 {G : Type u_2} {G' : Type u_1} [] [AddGroup G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ) :
= 0
theorem addMonoidHomOfForallMemZmultiples.proof_3 {G : Type u_2} {G' : Type u_1} [] [AddGroup G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ) (x : G) (y : G) :
{ toFun := fun (x : G) => , map_zero' := }.toFun (x + y) = { toFun := fun (x : G) => , map_zero' := }.toFun x + { toFun := fun (x : G) => , map_zero' := }.toFun y
theorem addMonoidHomOfForallMemZmultiples.proof_1 {G : Type u_1} [] {g : G} (hg : ∀ (x : G), ) (x : G) :
∃ (k : ), k g = x
noncomputable def addMonoidHomOfForallMemZmultiples {G : Type u_1} {G' : Type u_2} [] [AddGroup G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ) :
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
• = { toFun := fun (x : G) => , map_zero' := , map_add' := }
Instances For
noncomputable def monoidHomOfForallMemZpowers {G : Type u_1} {G' : Type u_2} [] [Group G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : 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
• = { toFun := fun (x : G) => , map_one' := , map_mul' := }
Instances For
@[simp]
theorem addMonoidHomOfForallMemZmultiples_apply_gen {G : Type u_1} {G' : Type u_2} [] [AddGroup G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ) :
() g = g'
@[simp]
theorem monoidHomOfForallMemZpowers_apply_gen {G : Type u_1} {G' : Type u_2} [] [Group G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : orderOf g' ) :
() g = g'
theorem AddMonoidHom.eq_iff_eq_on_generator {G : Type u_1} {G' : Type u_2} [] [AddGroup G'] {g : G} (hg : ∀ (x : 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'] {g : G} (hg : ∀ (x : 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'] {g : G} (hg : ∀ (x : 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'] {g : G} (hg : ∀ (x : 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'] {g : G} {g' : G'} (h : ) :
theorem addEquivOfAddOrderOfEq.proof_1 {G : Type u_2} {G' : Type u_1} [] [AddGroup G'] {g : G} {g' : G'} (h : ) :
noncomputable def addEquivOfAddOrderOfEq {G : Type u_1} {G' : Type u_2} [] [AddGroup G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ∀ (x : G'), ) (h : ) :
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'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ∀ (x : G'), ) (h : ) :
.comp =
theorem addEquivOfAddOrderOfEq.proof_3 {G : Type u_1} {G' : Type u_2} [] [AddGroup G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ∀ (x : G'), ) (h : ) :
.comp =
noncomputable def mulEquivOfOrderOfEq {G : Type u_1} {G' : Type u_2} [] [Group G'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ∀ (x : G'), ) (h : = 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'] {g : G} (hg : ∀ (x : G), ) {g' : G'} (hg' : ∀ (x : G'), ) (h : ) :