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) [AddGroup α] : Prop

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

• exists_generator : ∃ (g : α), ∀ (x : α), x ∈ AddSubgroup.zmultiples g

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

class IsCyclic (α : Type u) [Group α] : Prop

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

• exists_generator : ∃ (g : α), ∀ (x : α), x ∈ Subgroup.zpowers g

theorem IsCyclic.exists_generator {α : Type u} [Group α] [self : IsCyclic α] : ∃ (g : α), ∀ (x : α), x ∈ Subgroup.zpowers g

@[instance 100]

instance isAddCyclic_of_subsingleton {α : Type u} [AddGroup α] [Subsingleton α] : IsAddCyclic α

Equations

• ⋯ = ⋯

@[instance 100]

instance isCyclic_of_subsingleton {α : Type u} [Group α] [Subsingleton α] : IsCyclic α

Equations

• ⋯ = ⋯

@[simp]

theorem isCyclic_multiplicative_iff {α : Type u} [AddGroup α] : IsCyclic (Multiplicative α) ↔ IsAddCyclic α

instance isCyclic_multiplicative {α : Type u} [AddGroup α] [IsAddCyclic α] : IsCyclic (Multiplicative α)

Equations

• ⋯ = ⋯

@[simp]

theorem isAddCyclic_additive_iff {α : Type u} [Group α] : IsAddCyclic (Additive α) ↔ IsCyclic α

instance isAddCyclic_additive {α : Type u} [Group α] [IsCyclic α] : IsAddCyclic (Additive α)

Equations

• ⋯ = ⋯

theorem IsAddCyclic.addCommGroup.proof_1 {α : Type u_1} [hg : AddGroup α] [IsAddCyclic α] (x : α) (y : α) : x + y = y + x

def IsAddCyclic.addCommGroup {α : Type u} [hg : AddGroup α] [IsAddCyclic α] : AddCommGroup α

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

Equations

• IsAddCyclic.addCommGroup = AddCommGroup.mk ⋯

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

• ⋯ = ⋯

abbrev IsAddCyclic.addCommGroup.match_1 {α : Type u_1} [hg : AddGroup α] (y : α) : ∀ (w : α) (motive : y ∈ AddSubgroup.zmultiples w → Prop) (x : y ∈ AddSubgroup.zmultiples w), (∀ (w_1 : ℤ) (hm : (fun (x : ℤ) => x • w) w_1 = y), motive ⋯) → motive x

Equations

• ⋯ = ⋯

def IsCyclic.commGroup {α : Type u} [hg : Group α] [IsCyclic α] : CommGroup α

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

Equations

• IsCyclic.commGroup = CommGroup.mk ⋯

theorem Nontrivial.of_not_isAddCyclic {α : Type u} [AddGroup α] (nc : ¬IsAddCyclic α) : Nontrivial α

A non-cyclic additive group is non-trivial.

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

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 isAddCyclic_of_addOrderOf_eq_card {α : Type u} [AddGroup α] [Fintype α] (x : α) (hx : addOrderOf x = Fintype.card α) : IsAddCyclic α

theorem isCyclic_of_orderOf_eq_card {α : Type u} [Group α] [Fintype α] (x : α) (hx : orderOf x = Fintype.card α) : IsCyclic α

@[deprecated isAddCyclic_of_addOrderOf_eq_card]

theorem isAddCyclic_of_orderOf_eq_card {α : Type u} [AddGroup α] [Fintype α] (x : α) (hx : addOrderOf x = Fintype.card α) : IsAddCyclic α

Alias of isAddCyclic_of_addOrderOf_eq_card.

theorem AddSubgroup.eq_bot_or_eq_top_of_prime_card {G : Type u_1} [AddGroup G] : ∀ {x : Fintype G} (H : AddSubgroup G) [hp : Fact (Nat.Prime (Fintype.card G))], H = ⊥ ∨ H = ⊤

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 ≠ 0 → AddSubgroup.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 ≠ 1 → Subgroup.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 ≠ 0 → g' ∈ 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 ≠ 1 → g' ∈ 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 ≠ 0 → g' ∈ 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 ≠ 1 → g' ∈ 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 ≠ 0 → AddSubmonoid.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 ≠ 1 → Submonoid.powers g = ⊤

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

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) : IsCyclic α

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) : IsAddCyclic G

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) : IsCyclic G

theorem addOrderOf_eq_card_of_forall_mem_zmultiples {α : Type u} [AddGroup α] [Fintype α] {g : α} (hx : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) : addOrderOf g = Fintype.card α

theorem orderOf_eq_card_of_forall_mem_zpowers {α : Type u} [Group α] [Fintype α] {g : α} (hx : ∀ (x : α), x ∈ Subgroup.zpowers g) : orderOf g = Fintype.card α

theorem addOrderOf_generator_eq_natCard {α : Type u} {a : α} [AddGroup α] (h : ∀ (x : α), x ∈ AddSubgroup.zmultiples a) : addOrderOf a = Nat.card α

theorem orderOf_generator_eq_natCard {α : Type u} {a : α} [Group α] (h : ∀ (x : α), x ∈ Subgroup.zpowers a) : orderOf a = Nat.card α

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.addOrderOf_eq_zero_of_forall_mem_zmultiples {α : Type u} [AddGroup α] [Infinite α] {g : α} (h : ∀ (x : α), x ∈ AddSubgroup.zmultiples g) : addOrderOf g = 0

theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers {α : Type u} [Group α] [Infinite α] {g : α} (h : ∀ (x : α), x ∈ Subgroup.zpowers g) : orderOf g = 0

instance Bot.isAddCyclic {α : Type u} [AddGroup α] : IsAddCyclic ↥⊥

Equations

• ⋯ = ⋯

instance Bot.isCyclic {α : Type u} [Group α] : IsCyclic ↥⊥

Equations

• ⋯ = ⋯

instance AddSubgroup.isAddCyclic {α : Type u} [AddGroup α] [IsAddCyclic α] (H : AddSubgroup α) : IsAddCyclic ↥H

Equations

• ⋯ = ⋯

abbrev AddSubgroup.isAddCyclic.match_2 {α : Type u_1} [AddGroup α] (H : AddSubgroup α) (motive : ↥H → Prop) : ∀ (x : ↥H), (∀ (x : α) (hx : x ∈ H), motive ⟨x, hx⟩) → motive x

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

abbrev AddSubgroup.isAddCyclic.match_1 {α : Type u_1} [AddGroup α] (g : α) (x : α) (motive : x ∈ AddSubgroup.zmultiples g → Prop) : ∀ (x_1 : x ∈ AddSubgroup.zmultiples g), (∀ (k : ℤ) (hk : (fun (x : ℤ) => x • g) k = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

instance Subgroup.isCyclic {α : Type u} [Group α] [IsCyclic α] (H : Subgroup α) : IsCyclic ↥H

Equations

• ⋯ = ⋯

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

• ⋯ = ⋯

abbrev IsAddCyclic.card_nsmul_eq_zero_le.match_1 {α : Type u_1} [AddGroup α] (g : α) (x : α) (motive : x ∈ AddSubmonoid.multiples g → Prop) : ∀ (x_1 : x ∈ AddSubmonoid.multiples g), (∀ (m : ℕ) (hm : (fun (x : ℕ) => x • g) m = x), motive ⋯) → motive x_1

Equations

• ⋯ = ⋯

theorem IsAddCyclic.card_nsmul_eq_zero_le {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : ℕ} (hn0 : 0 < n) : (Finset.filter (fun (a : α) => n • a = 0) Finset.univ).card ≤ n

theorem IsCyclic.card_pow_eq_one_le {α : Type u} [Group α] [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) : (Finset.filter (fun (a : α) => a ^ n = 1) Finset.univ).card ≤ n

@[deprecated IsAddCyclic.card_nsmul_eq_zero_le]

theorem IsAddCyclic.card_pow_eq_one_le {α : Type u} [AddGroup α] [DecidableEq α] [Fintype α] [IsAddCyclic α] {n : ℕ} (hn0 : 0 < n) : (Finset.filter (fun (a : α) => n • a = 0) Finset.univ).card ≤ n

Alias of IsAddCyclic.card_nsmul_eq_zero_le.

theorem IsAddCyclic.exists_addMonoid_generator {α : Type u} [AddGroup α] [Finite α] [IsAddCyclic α] : ∃ (x : α), ∀ (y : α), y ∈ AddSubmonoid.multiples x

theorem IsCyclic.exists_monoid_generator {α : Type u} [Group α] [Finite α] [IsCyclic α] : ∃ (x : α), ∀ (y : α), y ∈ Submonoid.powers x

theorem IsAddCyclic.exists_ofOrder_eq_natCard {α : Type u} [AddGroup α] [h : IsAddCyclic α] : ∃ (g : α), addOrderOf g = Nat.card α

theorem IsCyclic.exists_ofOrder_eq_natCard {α : Type u} [Group α] [h : IsCyclic α] : ∃ (g : α), orderOf g = Nat.card α

theorem isAddCyclic_iff_exists_ofOrder_eq_natCard {α : Type u} [AddGroup α] [Finite α] : IsAddCyclic α ↔ ∃ (g : α), addOrderOf g = Nat.card α

theorem isCyclic_iff_exists_ofOrder_eq_natCard {α : Type u} [Group α] [Finite α] : IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α

@[deprecated]

theorem IsCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype {α : Type u} [Group α] [Finite α] : IsCyclic α ↔ ∃ (g : α), orderOf g = Nat.card α

Alias of isCyclic_iff_exists_ofOrder_eq_natCard.

@[deprecated]

theorem IsAddCyclic.iff_exists_ofOrder_eq_natCard_of_Fintype {α : Type u} [AddGroup α] [Finite α] : IsAddCyclic α ↔ ∃ (g : α), addOrderOf 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) : IsAddCyclic α

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).Nonempty → Prop) : ∀ (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

• ⋯ = ⋯

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) : IsCyclic α

@[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) : IsAddCyclic α

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) : IsSimpleAddGroup α

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) : IsSimpleGroup α

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

• ⋯ = ⋯

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

• ⋯ = ⋯

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) : AddCommGroup G

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

Equations

• commutativeOfAddCycleCenterQuotient f hf = let __src := let_fun this := inferInstance; this; AddCommGroup.mk ⋯

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) : CommGroup G

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

Equations

• commGroupOfCycleCenterQuotient f hf = let __src := let_fun this := inferInstance; this; CommGroup.mk ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

@[instance 100]

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

Equations

• ⋯ = ⋯

theorem IsSimpleAddGroup.prime_card {α : Type u} [AddCommGroup α] [IsSimpleAddGroup α] [Fintype α] : Nat.Prime (Fintype.card α)

theorem IsSimpleGroup.prime_card {α : Type u} [CommGroup α] [IsSimpleGroup α] [Fintype α] : Nat.Prime (Fintype.card α)

theorem AddCommGroup.is_simple_iff_isAddCyclic_and_prime_card {α : Type u} [Fintype α] [AddCommGroup α] : IsSimpleAddGroup α ↔ IsAddCyclic α ∧ Nat.Prime (Fintype.card α)

theorem CommGroup.is_simple_iff_isCyclic_and_prime_card {α : Type u} [Fintype α] [CommGroup α] : IsSimpleGroup α ↔ IsCyclic α ∧ Nat.Prime (Fintype.card α)

instance instIsAddCyclicInt : IsAddCyclic ℤ

Equations

• instIsAddCyclicInt = ⋯

instance ZMod.instIsAddCyclic (n : ℕ) : IsAddCyclic (ZMod n)

Equations

• ⋯ = ⋯

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

Equations

• ⋯ = ⋯

theorem IsAddCyclic.exponent_eq_card {α : Type u} [AddGroup α] [IsAddCyclic α] [Fintype α] : AddMonoid.exponent α = Fintype.card α

theorem IsCyclic.exponent_eq_card {α : Type u} [Group α] [IsCyclic α] [Fintype α] : Monoid.exponent α = Fintype.card α

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

• ⋯ = ⋯

theorem IsAddCyclic.of_exponent_eq_card {α : Type u} [AddCommGroup α] [Fintype α] (h : AddMonoid.exponent α = Fintype.card α) : IsAddCyclic α

theorem IsCyclic.of_exponent_eq_card {α : Type u} [CommGroup α] [Fintype α] (h : Monoid.exponent α = Fintype.card α) : IsCyclic α

theorem IsAddCyclic.iff_exponent_eq_card {α : Type u} [AddCommGroup α] [Fintype α] : IsAddCyclic α ↔ AddMonoid.exponent α = Fintype.card α

theorem IsCyclic.iff_exponent_eq_card {α : Type u} [CommGroup α] [Fintype α] : IsCyclic α ↔ Monoid.exponent α = Fintype.card α

theorem IsAddCyclic.exponent_eq_zero_of_infinite {α : Type u} [AddGroup α] [IsAddCyclic α] [Infinite α] : AddMonoid.exponent α = 0

theorem IsCyclic.exponent_eq_zero_of_infinite {α : Type u} [Group α] [IsCyclic α] [Infinite α] : Monoid.exponent α = 0

@[simp]

theorem ZMod.exponent (n : ℕ) : AddMonoid.exponent (ZMod n) = n

theorem not_isAddCyclic_iff_exponent_eq_prime {α : Type u} [AddGroup α] {p : ℕ} (hp : Nat.Prime p) (hα : Nat.card α = p ^ 2) : ¬IsAddCyclic α ↔ AddMonoid.exponent α = p

theorem not_isCyclic_iff_exponent_eq_prime {α : Type u} [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 zmultiplesHom_ker_eq {G : Type u_1} [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_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) : ZMod (Nat.card G) ≃+ 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.

noncomputable def zmodCyclicMulEquiv {G : Type u_1} [Group G] (h : IsCyclic G) : Multiplicative (ZMod (Nat.card G)) ≃* G

The isomorphism from Multiplicative (ZMod n) to any cyclic group of Nat.card equal to n.

Equations

• zmodCyclicMulEquiv h = AddEquiv.toMultiplicative (zmodAddCyclicAddEquiv ⋯)

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

• addEquivOfAddCyclicCardEq hcard = (hcard ▸ zmodAddCyclicAddEquiv hG).symm.trans (zmodAddCyclicAddEquiv hH)

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

• mulEquivOfCyclicCardEq hcard = (hcard ▸ zmodCyclicMulEquiv hG).symm.trans (zmodCyclicMulEquiv hH)

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

• addEquivOfPrimeCardEq hG hH = let_fun hGcyc := ⋯; let_fun hHcyc := ⋯; addEquivOfAddCyclicCardEq ⋯

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) : Nat.card G = Nat.card H

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

• mulEquivOfPrimeCardEq hG hH = let_fun hGcyc := ⋯; let_fun hHcyc := ⋯; mulEquivOfCyclicCardEq ⋯

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] [AddGroup G'] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {g' : G'} (hg' : addOrderOf g' ∣ addOrderOf g) : Classical.choose ⋯ • g' = 0

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

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

• addMonoidHomOfForallMemZmultiples hg hg' = { toFun := fun (x : G) => Classical.choose ⋯ • g', map_zero' := ⋯, map_add' := ⋯ }

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

• monoidHomOfForallMemZpowers hg hg' = { toFun := fun (x : G) => g' ^ Classical.choose ⋯, map_one' := ⋯, map_mul' := ⋯ }

@[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) : (addMonoidHomOfForallMemZmultiples hg hg') g = 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) : (monoidHomOfForallMemZpowers hg hg') g = g'

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

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

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

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

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

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

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

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

theorem addEquivOfAddOrderOfEq.proof_2 {G : Type u_1} {G' : Type u_2} [AddGroup G] [AddGroup G'] {g : G} {g' : G'} (h : addOrderOf g = addOrderOf g') : 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') : 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

• addEquivOfAddOrderOfEq hg hg' h = (addMonoidHomOfForallMemZmultiples hg ⋯).toAddEquiv (addMonoidHomOfForallMemZmultiples hg' ⋯) ⋯ ⋯

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') : (addMonoidHomOfForallMemZmultiples hg ⋯).comp (addMonoidHomOfForallMemZmultiples hg' ⋯) = AddMonoidHom.id 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') : (addMonoidHomOfForallMemZmultiples hg' ⋯).comp (addMonoidHomOfForallMemZmultiples hg ⋯) = AddMonoidHom.id 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

• mulEquivOfOrderOfEq hg hg' h = (monoidHomOfForallMemZpowers hg ⋯).toMulEquiv (monoidHomOfForallMemZpowers hg' ⋯) ⋯ ⋯

@[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') : (addEquivOfAddOrderOfEq hg hg' h).symm = addEquivOfAddOrderOfEq hg' hg ⋯

@[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