Documentation

theorem card_addOrderOf_eq_totient_aux₂ {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → {a : α | n • a = 0}.card ≤ n) {d : ℕ} (hd : d ∣ Fintype.card α) :

{a : α | addOrderOf a = d}.card = d.totient

theorem isCyclic_of_card_pow_eq_one_le {α : Type u_1} [Group α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → {a : α | a ^ n = 1}.card ≤ n) :

IsCyclic α

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

theorem isAddCyclic_of_card_nsmul_eq_zero_le {α : Type u_1} [AddGroup α] [DecidableEq α] [Fintype α] (hn : ∀ (n : ℕ), 0 < n → {a : α | n • a = 0}.card ≤ n) :

IsAddCyclic α

theorem IsCyclic.card_orderOf_eq_totient {α : Type u_1} [Group α] [IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) :

{a : α | orderOf a = d}.card = d.totient

theorem IsAddCyclic.card_addOrderOf_eq_totient {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) :

{a : α | addOrderOf a = d}.card = d.totient

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

IsSimpleGroup α

A finite group of prime order is simple.

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

IsSimpleAddGroup α

A finite group of prime order is simple.

theorem commutative_of_cyclic_center_quotient {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] [IsCyclic G'] (f : G →* G') (hf : f.ker ≤ Subgroup.center G) (a b : G) :

a * b = b * a

A group is commutative if the quotient by the center is cyclic. Also see commGroupOfCyclicCenterQuotient for the CommGroup instance.

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

a + b = b + a

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

@[implicit_reducible]

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

CommGroup G

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

Instances For

@[implicit_reducible]

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

AddCommGroup G

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

Instances For

@[instance 100]

instance IsSimpleGroup.isCyclic {α : Type u_1} [CommGroup α] [IsSimpleGroup α] :

IsCyclic α

@[instance 100]

instance IsSimpleAddGroup.isAddCyclic {α : Type u_1} [AddCommGroup α] [IsSimpleAddGroup α] :

IsAddCyclic α

theorem IsSimpleGroup.prime_card {α : Type u_1} [CommGroup α] [IsSimpleGroup α] :

Nat.Prime (Nat.card α)

theorem IsSimpleAddGroup.prime_card {α : Type u_1} [AddCommGroup α] [IsSimpleAddGroup α] :

Nat.Prime (Nat.card α)

theorem IsSimpleGroup.finite {α : Type u_1} [CommGroup α] [IsSimpleGroup α] :

Finite α

A commutative simple group is a finite group.

theorem IsSimpleAddGroup.finite {α : Type u_1} [AddCommGroup α] [IsSimpleAddGroup α] :

Finite α

A commutative simple group is a finite group.

theorem Group.is_simple_iff_prime_card {α : Type u_1} [Group α] [IsMulCommutative α] :

IsSimpleGroup α ↔ Nat.Prime (Nat.card α)

theorem AddGroup.is_simple_iff_prime_card {α : Type u_1} [AddGroup α] [IsAddCommutative α] :

IsSimpleAddGroup α ↔ Nat.Prime (Nat.card α)

theorem CommGroup.is_simple_iff_prime_card {α : Type u_1} [CommGroup α] :

IsSimpleGroup α ↔ Nat.Prime (Nat.card α)

theorem AddCommGroup.is_simple_iff_prime_card {α : Type u_1} [AddCommGroup α] :

IsSimpleAddGroup α ↔ Nat.Prime (Nat.card α)

@[deprecated CommGroup.is_simple_iff_prime_card (since := "2025-11-19")]

theorem CommGroup.is_simple_iff_isCyclic_and_prime_card {α : Type u_1} [CommGroup α] :

IsSimpleGroup α ↔ Nat.Prime (Nat.card α)

Alias of CommGroup.is_simple_iff_prime_card.

instance instIsAddCyclicInt :

IsAddCyclic ℤ

instance ZMod.instIsAddCyclic (n : ℕ) :

IsAddCyclic (ZMod n)

instance ZMod.instIsSimpleAddGroup {p : ℕ} [hp : Fact (Nat.Prime p)] :

IsSimpleAddGroup (ZMod p)

theorem LinearOrderedAddCommGroup.isAddCyclic_iff_nonempty_equiv_int {A : Type u_4} [AddCommGroup A] [LinearOrder A] [IsOrderedAddMonoid A] [Nontrivial A] :

IsAddCyclic A ↔ Nonempty (A ≃+o ℤ)

A linearly-ordered additive abelian group is cyclic iff it is isomorphic to ℤ as an ordered additive monoid.

theorem LinearOrderedCommGroup.isCyclic_iff_nonempty_equiv_int {G : Type u_4} [CommGroup G] [LinearOrder G] [IsOrderedMonoid G] [Nontrivial G] :

IsCyclic G ↔ Nonempty (G ≃*o Multiplicative ℤ)

A linearly-ordered abelian group is cyclic iff it is isomorphic to Multiplicative ℤ as an ordered monoid.

theorem IsCyclic.exponent_eq_card {α : Type u_1} [Group α] [IsCyclic α] :

Monoid.exponent α = Nat.card α

theorem IsAddCyclic.exponent_eq_card {α : Type u_1} [AddGroup α] [IsAddCyclic α] :

AddMonoid.exponent α = Nat.card α

theorem IsCyclic.of_exponent_eq_card {α : Type u_1} [CommGroup α] [Finite α] (h : Monoid.exponent α = Nat.card α) :

IsCyclic α

theorem IsAddCyclic.of_exponent_eq_card {α : Type u_1} [AddCommGroup α] [Finite α] (h : AddMonoid.exponent α = Nat.card α) :

IsAddCyclic α

theorem IsCyclic.iff_exponent_eq_card {α : Type u_1} [CommGroup α] [Finite α] :

IsCyclic α ↔ Monoid.exponent α = Nat.card α

theorem IsAddCyclic.iff_exponent_eq_card {α : Type u_1} [AddCommGroup α] [Finite α] :

IsAddCyclic α ↔ AddMonoid.exponent α = Nat.card α

theorem IsCyclic.exponent_eq_zero_of_infinite {α : Type u_1} [Group α] [IsCyclic α] [Infinite α] :

Monoid.exponent α = 0

theorem IsAddCyclic.exponent_eq_zero_of_infinite {α : Type u_1} [AddGroup α] [IsAddCyclic α] [Infinite α] :

AddMonoid.exponent α = 0

@[simp]

theorem ZMod.exponent (n : ℕ) :

AddMonoid.exponent (ZMod n) = n

theorem not_isCyclic_iff_exponent_eq_prime {α : Type u_1} [Group α] {p : ℕ} (hp : Nat.Prime p) (hα : Nat.card α = p ^ 2) :

¬IsCyclic α ↔ Monoid.exponent α = p

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

theorem not_isAddCyclic_iff_exponent_eq_prime {α : Type u_1} [AddGroup α] {p : ℕ} (hp : Nat.Prime p) (hα : Nat.card α = p ^ 2) :

¬IsAddCyclic α ↔ AddMonoid.exponent α = p

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

((zmultiplesHom G) g).ker = AddSubgroup.zmultiples ↑(addOrderOf g)

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

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

((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 zmodAddEquivOfGenerator {G : Type u_2} [AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ} (hn : Nat.card G = n) :

ZMod n ≃+ G

The isomorphism from ZMod n to any additive group of Nat.card equal to n generated by a single element g which sends 1 to g. See zmodAddCyclicAddEquiv for a version which doesn't take an explicit generator, and instead picks one out with the axiom of choice.

Instances For

@[simp]

theorem zmodAddEquivOfGenerator_apply_intCast {G : Type u_2} [AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ} (hn : Nat.card G = n) (i : ℤ) :

(zmodAddEquivOfGenerator hg hn) ↑i = i • g

@[simp]

theorem zmodAddEquivOfGenerator_symm_apply_zsmul {G : Type u_2} [AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ} (hn : Nat.card G = n) (i : ℤ) :

(zmodAddEquivOfGenerator hg hn).symm (i • g) = ↑i

@[simp]

theorem zmodAddEquivOfGenerator_apply_one {G : Type u_2} [AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ} (hn : Nat.card G = n) :

(zmodAddEquivOfGenerator hg hn) 1 = g

@[simp]

theorem zmodAddEquivOfGenerator_symm_apply_generator {G : Type u_2} [AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ} (hn : Nat.card G = n) :

(zmodAddEquivOfGenerator hg hn).symm g = 1

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

ZMod (Nat.card G) ≃+ G

An arbitrary isomorphism from ZMod n to any cyclic additive group of Nat.card equal to n. See zmodAddCyclicAddEquiv for a version which doesn't require an explicit generator, and instead picks one out with the axiom of choice.

Instances For

theorem exists_prime_addEquiv_ZMod {G : Type u_2} [CommGroup G] [IsSimpleGroup G] :

∃ (p : ℕ), Nat.Prime p ∧ Nonempty (Additive G ≃+ ZMod p)

A commutative simple group is isomorphic to ZMod p from some prime p.

noncomputable def zmodMulEquivOfGenerator {G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) :

Multiplicative (ZMod n) ≃* G

The isomorphism from Multiplicative (ZMod n) to any multiplicative group of Nat.card equal to n generated by a single element g which sends Multiplicative.ofAdd 1 to g. See zmodCyclicMulEquiv for a version which doesn't take an explicit generator, and instead picks one out with the axiom of choice.

Instances For

@[simp]

theorem zmodMulEquivOfGenerator_apply_ofAdd_intCast {G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (i : ℤ) :

(zmodMulEquivOfGenerator hg hn) (Multiplicative.ofAdd ↑i) = g ^ i

@[simp]

theorem zmodMulEquivOfGenerator_symm_apply_zpow {G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) (i : ℤ) :

(zmodMulEquivOfGenerator hg hn).symm (g ^ i) = Multiplicative.ofAdd ↑i

@[simp]

theorem zmodMulEquivOfGenerator_apply_ofAdd_one {G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) :

(zmodMulEquivOfGenerator hg hn) (Multiplicative.ofAdd 1) = g

@[simp]

theorem zmodMulEquivOfGenerator_symm_apply_generator {G : Type u_2} [Group G] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {n : ℕ} (hn : Nat.card G = n) :

(zmodMulEquivOfGenerator hg hn).symm g = Multiplicative.ofAdd 1

noncomputable def zmodCyclicMulEquiv {G : Type u_2} [Group G] (h : IsCyclic G) :

Multiplicative (ZMod (Nat.card G)) ≃* G

An arbitrary isomorphism from Multiplicative (ZMod n) to any cyclic group of Nat.card equal to n. See zmodMulEquivOfGenerator for a version which takes an explicit generator.

Instances For

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

G ≃+ G'

Two cyclic additive groups of the same cardinality are isomorphic.

Instances For

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

G ≃* G'

Two cyclic groups of the same cardinality are isomorphic.

Instances For

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

G ≃* G'

Two groups of the same prime cardinality are isomorphic.

Instances For

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

G ≃+ G'

Two additive groups of the same prime cardinality are isomorphic.

Instances For

theorem zpowersHom_bijective {G : Type u_2} [Infinite G] [Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) :

Function.Bijective ⇑((zpowersHom G) g)

noncomputable def intEquivOfZPowersEqTop {G : Type u_2} [Infinite G] [Group G] (g : G) (hg : Subgroup.zpowers g = ⊤) :

Multiplicative ℤ ≃* G

The isomorphism between Multiplicative ℤ and the infinite cyclic group G sending Multiplicative.ofAdd 1 to the generator g : G.

Instances For

@[simp]

theorem intEquivOfZPowersEqTop_apply {G : Type u_2} [Infinite G] [Group G] (g : G) (hg : Subgroup.zpowers g = ⊤) (a : Multiplicative ℤ) :

(intEquivOfZPowersEqTop g hg) a = g ^ Multiplicative.toAdd a

@[simp]

theorem intEquivOfZPowersEqTop_symm_self {G : Type u_2} [Infinite G] [Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) :

(intEquivOfZPowersEqTop g hg).symm g = Multiplicative.ofAdd 1

theorem mulintEquivOfZPowersEqTop_symm_apply_zpow {G : Type u_2} [Infinite G] [Group G] {g : G} (hg : Subgroup.zpowers g = ⊤) (k : ℤ) :

(intEquivOfZPowersEqTop g hg).symm (g ^ k) = Multiplicative.ofAdd k

theorem mulintEquivOfZPowersEqTop_strictMono {G : Type u_2} [Infinite G] [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] {g : G} (hg : Subgroup.zpowers g = ⊤) (hg1 : 1 < g) :

StrictMono ⇑(intEquivOfZPowersEqTop g hg)

theorem mulintEquivOfZPowersEqTop_strictAnti {G : Type u_2} [Infinite G] [CommGroup G] [PartialOrder G] [IsOrderedMonoid G] {g : G} (hg : Subgroup.zpowers g = ⊤) (hg1 : g < 1) :

StrictAnti ⇑(intEquivOfZPowersEqTop g hg)

@[reducible, inline]

noncomputable abbrev intCyclicMulEquiv {G : Type u_2} [Infinite G] [Group G] [IsCyclic G] :

Multiplicative ℤ ≃* G

An infinite cyclic group is isomorphic to Multiplicative ℤ.

Instances For

theorem zmultiplesHom_bijective {G : Type u_2} [Infinite G] [AddGroup G] {g : G} (hg : AddSubgroup.zmultiples g = ⊤) :

Function.Bijective ⇑((zmultiplesHom G) g)

noncomputable def intEquivOfZMultiplesEqTop {G : Type u_2} [Infinite G] [AddGroup G] (g : G) (hg : AddSubgroup.zmultiples g = ⊤) :

ℤ ≃+ G

The isomorphism between ℤ and the infinite cyclic group G sending 1 to the generator g : G.

Instances For

@[simp]

theorem intEquivOfZMultiplesEqTop_apply {G : Type u_2} [Infinite G] [AddGroup G] (g : G) (hg : AddSubgroup.zmultiples g = ⊤) (a : ℤ) :

(intEquivOfZMultiplesEqTop g hg) a = a • g

@[simp]

theorem intEquivOfZMultiplesEqTop_symm_self {G : Type u_2} [Infinite G] [AddGroup G] (g : G) (hg : AddSubgroup.zmultiples g = ⊤) :

(intEquivOfZMultiplesEqTop g hg).symm g = 1

theorem intEquivOfZMultiplesEqTop_symm_apply_zsmul {G : Type u_2} [Infinite G] [AddGroup G] {g : G} (hg : AddSubgroup.zmultiples g = ⊤) (k : ℤ) :

(intEquivOfZMultiplesEqTop g hg).symm (k • g) = k

@[reducible, inline]

noncomputable abbrev intCyclicAddEquiv {G : Type u_2} [Infinite G] [AddGroup G] [IsAddCyclic G] :

ℤ ≃+ G

An infinite cyclic additive group is isomorphic to ℤ.

Instances For

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

MulAut G ≃* (ZMod (Nat.card G))ˣ

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

Instances For

@[simp]

theorem IsCyclic.val_inv_mulAutMulEquiv_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : MulAut G) :

↑((mulAutMulEquiv G) a✝)⁻¹ = Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm ((MulEquiv.symm a✝) ((zmodCyclicMulEquiv h) (Multiplicative.ofAdd 1))))

@[simp]

theorem IsCyclic.mulAutMulEquiv_symm_apply_symm_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : (ZMod (Nat.card G))ˣ) (a✝¹ : G) :

(MulEquiv.symm ((mulAutMulEquiv G).symm a✝)) a✝¹ = (zmodCyclicMulEquiv h) (Multiplicative.ofAdd (a✝⁻¹ • Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a✝¹)))

@[simp]

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

((mulAutMulEquiv G).symm a✝) a✝¹ = (zmodCyclicMulEquiv h) (Multiplicative.ofAdd (a✝ • Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm a✝¹)))

@[simp]

theorem IsCyclic.val_mulAutMulEquiv_apply (G : Type u_2) [Group G] [h : IsCyclic G] (a✝ : MulAut G) :

↑((mulAutMulEquiv G) a✝) = Multiplicative.toAdd ((zmodCyclicMulEquiv h).symm (a✝ ((zmodCyclicMulEquiv h) (Multiplicative.ofAdd 1))))

theorem IsCyclic.card_mulAut (G : Type u_2) [Group G] [Finite G] [h : IsCyclic G] :

Nat.card (MulAut G) = (Nat.card G).totient

theorem IsCyclic.card_powMonoidHom_range (G : Type u_2) [CommGroup G] [hG : IsCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(powMonoidHom d).range = Nat.card G / (Nat.card G).gcd d

theorem IsAddCyclic.card_nsmulAddMonoidHom_range (G : Type u_2) [AddCommGroup G] [hG : IsAddCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(nsmulAddMonoidHom d).range = Nat.card G / (Nat.card G).gcd d

theorem IsCyclic.index_powMonoidHom_ker (G : Type u_2) [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :

(powMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d

theorem IsAddCyclic.index_nsmulAddMonoidHom_ker (G : Type u_2) [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) :

(nsmulAddMonoidHom d).ker.index = Nat.card G / (Nat.card G).gcd d

theorem IsCyclic.card_powMonoidHom_ker (G : Type u_2) [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(powMonoidHom d).ker = (Nat.card G).gcd d

theorem IsAddCyclic.card_nsmulAddMonoidHom_ker (G : Type u_2) [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) :

Nat.card ↥(nsmulAddMonoidHom d).ker = (Nat.card G).gcd d

theorem IsCyclic.index_powMonoidHom_range (G : Type u_2) [CommGroup G] [IsCyclic G] [Finite G] (d : ℕ) :

(powMonoidHom d).range.index = (Nat.card G).gcd d

theorem IsAddCyclic.index_nsmulAddMonoidHom_range (G : Type u_2) [AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ) :

(nsmulAddMonoidHom d).range.index = (Nat.card G).gcd d

Groups with a given generator #

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

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

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

G →* G'

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

Instances For

noncomputable def addMonoidHomOfForallMemZMultiples {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' ∣ addOrderOf g) :

G →+ G'

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

Instances For

@[simp]

theorem monoidHomOfForallMemZpowers_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : orderOf g' ∣ orderOf g) :

(monoidHomOfForallMemZpowers hg hg') g = g'

@[simp]

theorem addMonoidHomOfForallMemZMultiples_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' ∣ addOrderOf g) :

(addMonoidHomOfForallMemZMultiples hg hg') g = g'

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

f₁ = f₂ ↔ f₁ g = f₂ g

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

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

f₁ = f₂ ↔ f₁ g = f₂ g

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

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

f₁ = f₂ ↔ f₁ g = f₂ g

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

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

f₁ = f₂ ↔ f₁ g = f₂ g

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

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

G ≃* G'

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

Instances For

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

G ≃+ G'

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

Instances For

@[simp]

theorem mulEquivOfOrderOfEq_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') :

(mulEquivOfOrderOfEq hg hg' h) g = g'

@[simp]

theorem addEquivOfAddOrderOfEq_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :

(addEquivOfAddOrderOfEq hg hg' h) g = g'

@[simp]

theorem mulEquivOfOrderOfEq_symm {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') :

(mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg ⋯

@[simp]

theorem addEquivOfAddOrderOfEq_symm {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :

(addEquivOfAddOrderOfEq hg hg' h).symm = addEquivOfAddOrderOfEq hg' hg ⋯

theorem mulEquivOfOrderOfEq_symm_apply_gen {G : Type u_2} {G' : Type u_3} [Group G] [Group G'] {g : G} (hg : ∀ (x : G), x ∈ Subgroup.zpowers g) {g' : G'} (hg' : ∀ (x : G'), x ∈ Subgroup.zpowers g') (h : orderOf g = orderOf g') :

(mulEquivOfOrderOfEq hg hg' h).symm g' = g

theorem addEquivOfAddOrderOfEq_symm_apply_gen {G : Type u_2} {G' : Type u_3} [AddGroup G] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : ∀ (x : G'), x ∈ AddSubgroup.zmultiples g') (h : addOrderOf g = addOrderOf g') :

(addEquivOfAddOrderOfEq hg hg' h).symm g' = g

theorem Group.isCyclic_of_coprime_card_range_card_ker {M : Type u_4} {N : Type u_5} [CommGroup M] [Group N] (f : M →* N) (h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)) [IsCyclic ↥f.ker] [IsCyclic ↥f.range] :

IsCyclic M

theorem AddGroup.isAddCyclic_of_coprime_card_range_card_ker {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddGroup N] (f : M →+ N) (h : (Nat.card ↥f.ker).Coprime (Nat.card ↥f.range)) [IsAddCyclic ↥f.ker] [IsAddCyclic ↥f.range] :

IsAddCyclic M

theorem Group.isCyclic_of_coprime_card_ker {M : Type u_4} {N : Type u_5} [CommGroup M] [Group N] (f : M →* N) (h : (Nat.card ↥f.ker).Coprime (Nat.card N)) [IsCyclic ↥f.ker] [hN : IsCyclic N] (hf : Function.Surjective ⇑f) :

IsCyclic M

theorem AddGroup.isAddCyclic_of_coprime_card_ker {M : Type u_4} {N : Type u_5} [AddCommGroup M] [AddGroup N] (f : M →+ N) (h : (Nat.card ↥f.ker).Coprime (Nat.card N)) [IsAddCyclic ↥f.ker] [hN : IsAddCyclic N] (hf : Function.Surjective ⇑f) :

IsAddCyclic M

theorem isCyclic_left_of_prod (M : Type u_4) (N : Type u_5) [Group M] [Group N] [cyc : IsCyclic (M × N)] :

IsCyclic M

theorem isAddCyclic_left_of_prod (M : Type u_4) (N : Type u_5) [AddGroup M] [AddGroup N] [cyc : IsAddCyclic (M × N)] :

IsAddCyclic M

theorem isCyclic_right_of_prod (M : Type u_4) (N : Type u_5) [Group M] [Group N] [cyc : IsCyclic (M × N)] :

IsCyclic N

theorem isAddCyclic_right_of_prod (M : Type u_4) (N : Type u_5) [AddGroup M] [AddGroup N] [cyc : IsAddCyclic (M × N)] :

IsAddCyclic N

theorem coprime_card_of_isCyclic_prod (M : Type u_4) (N : Type u_5) [Group M] [Group N] [cyc : IsCyclic (M × N)] [Finite M] [Finite N] :

(Nat.card M).Coprime (Nat.card N)

theorem coprime_card_of_isAddCyclic_prod (M : Type u_4) (N : Type u_5) [AddGroup M] [AddGroup N] [cyc : IsAddCyclic (M × N)] [Finite M] [Finite N] :

(Nat.card M).Coprime (Nat.card N)

theorem not_isAddCyclic_prod_of_infinite_nontrivial (M : Type u_4) (N : Type u_5) [AddGroup M] [AddGroup N] [Infinite M] [Nontrivial N] :

¬IsAddCyclic (M × N)

theorem not_isCyclic_prod_of_infinite_nontrivial (M : Type u_4) (N : Type u_5) [Group M] [Group N] [Infinite M] [Nontrivial N] :

¬IsCyclic (M × N)

theorem Group.isCyclic_prod_iff {M : Type u_4} {N : Type u_5} [Group M] [Group N] :

IsCyclic (M × N) ↔ IsCyclic M ∧ IsCyclic N ∧ (Nat.card M).Coprime (Nat.card N)

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

theorem AddGroup.isAddCyclic_prod_iff {M : Type u_4} {N : Type u_5} [AddGroup M] [AddGroup N] :

IsAddCyclic (M × N) ↔ IsAddCyclic M ∧ IsAddCyclic N ∧ (Nat.card M).Coprime (Nat.card N)

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