doc-next-gen

Mathlib.GroupTheory.SpecificGroups.Cyclic

Module docstring

{"# 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 ","### 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. "}

IsCyclic.exists_generator theorem
[Group α] [IsCyclic α] : ∃ g : α, ∀ x, x ∈ zpowers g
Full source 
@[to_additive]
theorem IsCyclic.exists_generator [Group α] [IsCyclic α] : ∃ g : α, ∀ x, x ∈ zpowers g :=
  exists_zpow_surjective α
Existence of a Generator for Cyclic Groups
Informal description
For any cyclic group $\alpha$, there exists an element $g \in \alpha$ such that every element $x \in \alpha$ belongs to the subgroup generated by $g$, i.e., $x \in \{g^n \mid n \in \mathbb{Z}\}$.
isCyclic_iff_exists_zpowers_eq_top theorem
[Group α] : IsCyclic α ↔ ∃ g : α, zpowers g = ⊤
Full source 
@[to_additive]
theorem isCyclic_iff_exists_zpowers_eq_top [Group α] : IsCyclicIsCyclic α ↔ ∃ g : α, zpowers g = ⊤ := by
  simp only [eq_top_iff', mem_zpowers_iff]
  exact ⟨fun ⟨h⟩ ↦ h, fun h ↦ ⟨h⟩⟩
Characterization of Cyclic Groups via Generators
Informal description
A group $G$ is cyclic if and only if there exists an element $g \in G$ such that the subgroup generated by $g$ (i.e., $\{g^n \mid n \in \mathbb{Z}\}$) equals the entire group $G$.
Subgroup.isCyclic_iff_exists_zpowers_eq_top theorem
[Group α] (H : Subgroup α) : IsCyclic H ↔ ∃ g : α, Subgroup.zpowers g = H
Full source 
@[to_additive]
protected theorem Subgroup.isCyclic_iff_exists_zpowers_eq_top [Group α] (H : Subgroup α) :
    IsCyclicIsCyclic H ↔ ∃ g : α, Subgroup.zpowers g = H := by
  rw [isCyclic_iff_exists_zpowers_eq_top]
  simp_rw [← (map_injective H.subtype_injective).eq_iff, ← MonoidHom.range_eq_map,
    H.range_subtype, MonoidHom.map_zpowers, Subtype.exists, coe_subtype, exists_prop]
  exact exists_congr fun g ↦ and_iff_right_of_imp fun h ↦ h ▸ mem_zpowers g
Characterization of Cyclic Subgroups via Generators
Informal description
A subgroup $H$ of a group $G$ is cyclic if and only if there exists an element $g \in G$ such that $H$ is equal to the subgroup generated by $g$, i.e., $H = \{g^n \mid n \in \mathbb{Z}\}$.
isCyclic_multiplicative_iff theorem
[SubNegMonoid α] : IsCyclic (Multiplicative α) ↔ IsAddCyclic α
Full source 
@[simp]
theorem isCyclic_multiplicative_iff [SubNegMonoid α] :
    IsCyclicIsCyclic (Multiplicative α) ↔ IsAddCyclic α :=
  ⟨fun H ↦ ⟨H.1⟩, fun H ↦ ⟨H.1⟩⟩
Cyclicity Equivalence Between Multiplicative and Additive Groups
Informal description
Let $\alpha$ be a subtraction-negation monoid. Then the multiplicative group of $\alpha$ is cyclic if and only if the additive group of $\alpha$ is cyclic.
isAddCyclic_additive_iff theorem
[DivInvMonoid α] : IsAddCyclic (Additive α) ↔ IsCyclic α
Full source 
@[simp]
theorem isAddCyclic_additive_iff [DivInvMonoid α] : IsAddCyclicIsAddCyclic (Additive α) ↔ IsCyclic α :=
  ⟨fun H ↦ ⟨H.1⟩, fun H ↦ ⟨H.1⟩⟩
Cyclicity Equivalence Between Additive and Multiplicative Groups
Informal description
For any division-inversion monoid $\alpha$, the additive group of $\alpha$ is cyclic if and only if the multiplicative group of $\alpha$ is cyclic.
IsCyclic.commutative instance
[Group α] [IsCyclic α] : Std.Commutative (· * · : α → α → α)
Full source 
@[to_additive]
instance IsCyclic.commutative [Group α] [IsCyclic α] :
    Std.Commutative (· * · : α → α → α) where
  comm x y :=
    let ⟨_, hg⟩ := IsCyclic.exists_generator (α := α)
    let ⟨_, hx⟩ := hg x
    let ⟨_, hy⟩ := hg y
    hy ▸ hx ▸ zpow_mul_comm _ _ _
Cyclic Groups are Commutative
Informal description
Every cyclic group is commutative. That is, for any group $\alpha$ that is cyclic, the multiplication operation on $\alpha$ is commutative: $x \cdot y = y \cdot x$ for all $x, y \in \alpha$.
IsCyclic.commGroup definition
[hg : Group α] [IsCyclic α] : CommGroup α
Full source 
/-- A cyclic group is always commutative. This is not an `instance` because often we have a better
proof of `CommGroup`. -/
@[to_additive
      "A cyclic group is always commutative. This is not an `instance` because often we have
      a better proof of `AddCommGroup`."]
def IsCyclic.commGroup [hg : Group α] [IsCyclic α] : CommGroup α :=
  { hg with mul_comm := commutative.comm }
Commutative group structure on a cyclic group
Informal description
For any group $\alpha$ that is cyclic, the structure of a commutative group can be derived, where the binary operation is commutative. That is, for all $x, y \in \alpha$, we have $x * y = y * x$.
instIsMulCommutativeSubtypeMemSubgroupOfIsCyclic instance
[Group G] (H : Subgroup G) [IsCyclic H] : IsMulCommutative H
Full source 
instance [Group G] (H : Subgroup G) [IsCyclic H] : IsMulCommutative H :=
  ⟨IsCyclic.commutative⟩
Multiplication in Cyclic Subgroups is Commutative
Informal description
For any group $G$ and any subgroup $H$ of $G$, if $H$ is cyclic, then the multiplication operation on $H$ is commutative.
Nontrivial.of_not_isCyclic theorem
(nc : ¬IsCyclic α) : Nontrivial α
Full source 
/-- A non-cyclic multiplicative group is non-trivial. -/
@[to_additive "A non-cyclic additive group is non-trivial."]
theorem Nontrivial.of_not_isCyclic (nc : ¬IsCyclic α) : Nontrivial α := by
  contrapose! nc
  exact @isCyclic_of_subsingleton _ _ (not_nontrivial_iff_subsingleton.mp nc)
Non-cyclic groups are nontrivial
Informal description
If a group $\alpha$ is not cyclic, then it is nontrivial (i.e., it contains at least two distinct elements).
MonoidHom.map_cyclic theorem
[h : IsCyclic G] (σ : G →* G) : ∃ m : ℤ, ∀ g : G, σ g = g ^ m
Full source 
@[to_additive]
theorem MonoidHom.map_cyclic [h : IsCyclic G] (σ : G →* G) :
    ∃ m : ℤ, ∀ g : G, σ g = g ^ m := by
  obtain ⟨h, hG⟩ := IsCyclic.exists_generator (α := G)
  obtain ⟨m, hm⟩ := hG (σ h)
  refine ⟨m, fun g => ?_⟩
  obtain ⟨n, rfl⟩ := hG g
  rw [MonoidHom.map_zpow, ← hm, ← zpow_mul, ← zpow_mul']
Endomorphisms of Cyclic Groups are Power Maps
Informal description
Let $G$ be a cyclic group. For any endomorphism $\sigma \colon G \to G$, there exists an integer $m$ such that $\sigma(g) = g^m$ for all $g \in G$.
isCyclic_iff_exists_orderOf_eq_natCard theorem
[Finite α] : IsCyclic α ↔ ∃ g : α, orderOf g = Nat.card α
Full source 
@[to_additive]
lemma isCyclic_iff_exists_orderOf_eq_natCard [Finite α] :
    IsCyclicIsCyclic α ↔ ∃ g : α, orderOf g = Nat.card α := by
  simp_rw [isCyclic_iff_exists_zpowers_eq_top, ← card_eq_iff_eq_top, Nat.card_zpowers]
Characterization of Finite Cyclic Groups via Element Order and Cardinality
Informal description
A finite group $\alpha$ is cyclic if and only if there exists an element $g \in \alpha$ whose order equals the cardinality of $\alpha$.
isCyclic_iff_exists_natCard_le_orderOf theorem
[Finite α] : IsCyclic α ↔ ∃ g : α, Nat.card α ≤ orderOf g
Full source 
@[to_additive]
lemma isCyclic_iff_exists_natCard_le_orderOf [Finite α] :
    IsCyclicIsCyclic α ↔ ∃ g : α, Nat.card α ≤ orderOf g := by
  rw [isCyclic_iff_exists_orderOf_eq_natCard]
  apply exists_congr
  intro g
  exact ⟨Eq.ge, le_antisymm orderOf_le_card⟩
Characterization of Finite Cyclic Groups via Cardinality and Element Order
Informal description
A finite group $\alpha$ is cyclic if and only if there exists an element $g \in \alpha$ such that the cardinality of $\alpha$ is less than or equal to the order of $g$.
isCyclic_of_orderOf_eq_card theorem
[Finite α] (x : α) (hx : orderOf x = Nat.card α) : IsCyclic α
Full source 
@[to_additive]
theorem isCyclic_of_orderOf_eq_card [Finite α] (x : α) (hx : orderOf x = Nat.card α) :
    IsCyclic α :=
  isCyclic_iff_exists_orderOf_eq_natCard.mpr ⟨x, hx⟩
Finite Group is Cyclic if Element Order Equals Group Cardinality
Informal description
Let $G$ be a finite group. If there exists an element $g \in G$ whose order equals the cardinality of $G$, then $G$ is cyclic.
isCyclic_of_card_le_orderOf theorem
[Finite α] (x : α) (hx : Nat.card α ≤ orderOf x) : IsCyclic α
Full source 
@[to_additive]
theorem isCyclic_of_card_le_orderOf [Finite α] (x : α) (hx : Nat.card α ≤ orderOf x) :
    IsCyclic α :=
  isCyclic_iff_exists_natCard_le_orderOf.mpr ⟨x, hx⟩
Finite Group is Cyclic if Cardinality Bounded by Element Order
Informal description
Let $G$ be a finite group and let $x \in G$ be an element such that the cardinality of $G$ is less than or equal to the order of $x$. Then $G$ is cyclic.
zpowers_eq_top_of_prime_card theorem
{p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) : zpowers g = ⊤
Full source 
/-- Any non-identity element of a finite group of prime order generates the group. -/
@[to_additive "Any non-identity element of a finite group of prime order generates the group."]
theorem zpowers_eq_top_of_prime_card {p : ℕ}
    [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) : zpowers g = ⊤ := by
  subst h
  have := (zpowers g).eq_bot_or_eq_top_of_prime_card
  rwa [zpowers_eq_bot, or_iff_right hg] at this
Prime Order Group is Generated by Any Non-Identity Element
Informal description
Let $G$ be a finite group of prime order $p$, and let $g \in G$ be a non-identity element. Then the subgroup generated by $g$ is the entire group $G$, i.e., $\langle g \rangle = G$.
mem_zpowers_of_prime_card theorem
{p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) : g' ∈ zpowers g
Full source 
@[to_additive]
theorem mem_zpowers_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) : g' ∈ zpowers g := by
  simp_rw [zpowers_eq_top_of_prime_card h hg, Subgroup.mem_top]
Every Element is a Power in a Prime Order Group
Informal description
Let $G$ be a finite group of prime order $p$, and let $g \in G$ be a non-identity element. Then every element $g' \in G$ is a power of $g$, i.e., $g' \in \langle g \rangle$.
mem_powers_of_prime_card theorem
{p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) : g' ∈ Submonoid.powers g
Full source 
@[to_additive]
theorem mem_powers_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card G = p) {g g' : G} (hg : g ≠ 1) : g' ∈ Submonoid.powers g := by
  have : Finite G := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
  rw [mem_powers_iff_mem_zpowers]
  exact mem_zpowers_of_prime_card h hg
Every Element is a Natural Power in a Prime Order Group
Informal description
Let $G$ be a finite group of prime order $p$, and let $g \in G$ be a non-identity element. Then every element $g' \in G$ belongs to the submonoid generated by $g$, i.e., $g' \in \{g^n \mid n \in \mathbb{N}\}$.
powers_eq_top_of_prime_card theorem
{p : ℕ} [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) : Submonoid.powers g = ⊤
Full source 
@[to_additive]
theorem powers_eq_top_of_prime_card {p : ℕ}
    [hp : Fact p.Prime] (h : Nat.card G = p) {g : G} (hg : g ≠ 1) : Submonoid.powers g = ⊤ := by
  ext x
  simp [mem_powers_of_prime_card h hg]
Submonoid of Powers Equals Group for Prime Order
Informal description
Let $G$ be a finite group of prime order $p$, and let $g \in G$ be a non-identity element. Then the submonoid generated by $g$ is equal to the entire group $G$, i.e., $\{g^n \mid n \in \mathbb{N}\} = G$.
isCyclic_of_prime_card theorem
{p : ℕ} [hp : Fact p.Prime] (h : Nat.card α = p) : IsCyclic α
Full source 
/-- A finite group of prime order is cyclic. -/
@[to_additive "A finite group of prime order is cyclic."]
theorem isCyclic_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card α = p) : IsCyclic α := by
  have : Finite α := Nat.finite_of_card_ne_zero (h ▸ hp.1.ne_zero)
  have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp (h ▸ hp.1.one_lt)
  obtain ⟨g, hg⟩ : ∃ g : α, g ≠ 1 := exists_ne 1
  exact ⟨g, fun g' ↦ mem_zpowers_of_prime_card h hg⟩
Finite Groups of Prime Order are Cyclic
Informal description
Let $G$ be a finite group of prime order $p$. Then $G$ is cyclic.
isCyclic_of_card_dvd_prime theorem
{p : ℕ} [hp : Fact p.Prime] (h : Nat.card α ∣ p) : IsCyclic α
Full source 
/-- A finite group of order dividing a prime is cyclic. -/
@[to_additive "A finite group of order dividing a prime is cyclic."]
theorem isCyclic_of_card_dvd_prime {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.cardNat.card α ∣ p) : IsCyclic α := by
  rcases (Nat.dvd_prime hp.out).mp h with h | h
  · exact @isCyclic_of_subsingleton α _ (Nat.card_eq_one_iff_unique.mp h).1
  · exact isCyclic_of_prime_card h
Finite Groups with Order Dividing a Prime are Cyclic
Informal description
Let $G$ be a finite group whose order divides a prime number $p$. Then $G$ is cyclic.
isCyclic_of_surjective theorem
{F : Type*} [hH : IsCyclic G'] [FunLike F G' G] [MonoidHomClass F G' G] (f : F) (hf : Function.Surjective f) : IsCyclic G
Full source 
@[to_additive]
theorem isCyclic_of_surjective {F : Type*} [hH : IsCyclic G']
    [FunLike F G' G] [MonoidHomClass F G' G] (f : F) (hf : Function.Surjective f) :
    IsCyclic G := by
  obtain ⟨x, hx⟩ := hH
  refine ⟨f x, fun a ↦ ?_⟩
  obtain ⟨a, rfl⟩ := hf a
  obtain ⟨n, rfl⟩ := hx a
  exact ⟨n, (map_zpow _ _ _).symm⟩
Surjective Homomorphism Preserves Cyclicity: If $G'$ is cyclic and $f \colon G' \to G$ is a surjective homomorphism, then $G$ is cyclic.
Informal description
Let $G'$ be a cyclic group, $G$ be another group, and $F$ be a type of homomorphisms from $G'$ to $G$ that preserve the group structure. If there exists a surjective homomorphism $f \colon G' \to G$, then $G$ is also cyclic.
orderOf_eq_card_of_forall_mem_zpowers theorem
{g : α} (hx : ∀ x, x ∈ zpowers g) : orderOf g = Nat.card α
Full source 
@[to_additive]
theorem orderOf_eq_card_of_forall_mem_zpowers {g : α} (hx : ∀ x, x ∈ zpowers g) :
    orderOf g = Nat.card α := by
  rw [← Nat.card_zpowers, (zpowers g).eq_top_iff'.mpr hx, card_top]
Order of Generator Equals Group Cardinality in Cyclic Groups
Informal description
Let $G$ be a group and $g \in G$ be an element such that every element of $G$ is in the subgroup generated by $g$ (i.e., $G = \langle g \rangle$). Then the order of $g$ equals the cardinality of $G$ as a natural number. In other words, $\text{orderOf}(g) = |G|$.
exists_pow_ne_one_of_isCyclic theorem
[G_cyclic : IsCyclic G] {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) : ∃ a : G, a ^ k ≠ 1
Full source 
@[to_additive]
theorem exists_pow_ne_one_of_isCyclic [G_cyclic : IsCyclic G]
    {k : ℕ} (k_pos : k ≠ 0) (k_lt_card_G : k < Nat.card G) : ∃ a : G, a ^ k ≠ 1 := by
  have : Finite G := Nat.finite_of_card_ne_zero (Nat.ne_zero_of_lt k_lt_card_G)
  rcases G_cyclic with ⟨a, ha⟩
  use a
  contrapose! k_lt_card_G
  convert orderOf_le_of_pow_eq_one k_pos.bot_lt k_lt_card_G
  rw [← Nat.card_zpowers, eq_comm, card_eq_iff_eq_top, eq_top_iff]
  exact fun x _ ↦ ha x
Existence of Non-Identity $k$-th Power in Finite Cyclic Groups
Informal description
Let $G$ be a finite cyclic group and let $k$ be a positive integer such that $k < |G|$. Then there exists an element $a \in G$ such that $a^k \neq 1$.
Infinite.orderOf_eq_zero_of_forall_mem_zpowers theorem
[Infinite α] {g : α} (h : ∀ x, x ∈ zpowers g) : orderOf g = 0
Full source 
@[to_additive]
theorem Infinite.orderOf_eq_zero_of_forall_mem_zpowers [Infinite α] {g : α}
    (h : ∀ x, x ∈ zpowers g) : orderOf g = 0 := by
  rw [orderOf_eq_card_of_forall_mem_zpowers h, Nat.card_eq_zero_of_infinite]
Order of Generator in Infinite Cyclic Group is Zero
Informal description
Let $G$ be an infinite group and $g \in G$ be an element such that every element of $G$ is in the cyclic subgroup generated by $g$ (i.e., $G = \langle g \rangle$). Then the order of $g$ is zero.
Subgroup.isCyclic instance
[IsCyclic α] (H : Subgroup α) : IsCyclic H
Full source 
@[to_additive]
instance Subgroup.isCyclic [IsCyclic α] (H : Subgroup α) : IsCyclic H :=
  haveI := Classical.propDecidable
  let ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
  if hx : ∃ x : α, x ∈ H ∧ x ≠ (1 : α) then
    let ⟨x, hx₁, hx₂⟩ := hx
    let ⟨k, hk⟩ := hg x
    have hk : g ^ k = x := hk
    have hex : ∃ n : ℕ, 0 < n ∧ g ^ n ∈ H :=
      ⟨k.natAbs,
        Nat.pos_of_ne_zero fun h => hx₂ <| by
          rw [← hk, Int.natAbs_eq_zero.mp h, zpow_zero], by
            rcases k with k | k
            · rw [Int.ofNat_eq_coe, Int.natAbs_cast k, ← zpow_natCast, ← Int.ofNat_eq_coe, hk]
              exact hx₁
            · rw [Int.natAbs_negSucc, ← Subgroup.inv_mem_iff H]; simp_all⟩
    ⟨⟨⟨g ^ Nat.find hex, (Nat.find_spec hex).2⟩, fun ⟨x, hx⟩ =>
        let ⟨k, hk⟩ := hg x
        have hk : g ^ k = x := hk
        have hk₂ : g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) ∈ H := by
          rw [zpow_mul]
          apply H.zpow_mem
          exact mod_cast (Nat.find_spec hex).2
        have hk₃ : g ^ (k % Nat.find hex : ℤ) ∈ H :=
          (Subgroup.mul_mem_cancel_right H hk₂).1 <| by
            rw [← zpow_add, Int.emod_add_ediv, hk]; exact hx
        have hk₄ : k % Nat.find hex = (k % Nat.find hex).natAbs := by
          rw [Int.natAbs_of_nonneg
              (Int.emod_nonneg _ (Int.natCast_ne_zero_iff_pos.2 (Nat.find_spec hex).1))]
        have hk₅ : g ^ (k % Nat.find hex).natAbs ∈ H := by rwa [← zpow_natCast, ← hk₄]
        have hk₆ : (k % (Nat.find hex : ℤ)).natAbs = 0 :=
          by_contradiction fun h =>
            Nat.find_min hex
              (Int.ofNat_lt.1 <| by
                rw [← hk₄]; exact Int.emod_lt_of_pos _ (Int.natCast_pos.2 (Nat.find_spec hex).1))
              ⟨Nat.pos_of_ne_zero h, hk₅⟩
        ⟨k / (Nat.find hex : ℤ),
          Subtype.ext_iff_val.2
            (by
              suffices g ^ ((Nat.find hex : ℤ) * (k / Nat.find hex : ℤ)) = x by simpa [zpow_mul]
              rw [Int.mul_ediv_cancel'
                  (Int.dvd_of_emod_eq_zero (Int.natAbs_eq_zero.mp hk₆)),
                hk])⟩⟩⟩
  else by
    have : H = (⊥ : Subgroup α) :=
      Subgroup.ext fun x =>
        ⟨fun h => by simp at *; tauto, fun h => by rw [Subgroup.mem_bot.1 h]; exact H.one_mem⟩
    subst this; infer_instance
Subgroups of Cyclic Groups are Cyclic
Informal description
Every subgroup of a cyclic group is cyclic.
isCyclic_of_injective theorem
[IsCyclic G'] (f : G →* G') (hf : Function.Injective f) : IsCyclic G
Full source 
@[to_additive]
theorem isCyclic_of_injective [IsCyclic G'] (f : G →* G') (hf : Function.Injective f) :
    IsCyclic G :=
  isCyclic_of_surjective (MonoidHom.ofInjective hf).symm (MonoidHom.ofInjective hf).symm.surjective
Injective Homomorphism Preserves Cyclicity
Informal description
Let $G$ and $G'$ be groups, with $G'$ cyclic. If there exists an injective group homomorphism $f \colon G \to G'$, then $G$ is also cyclic.
IsCyclic.card_pow_eq_one_le theorem
[DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) : #{a : α | a ^ n = 1} ≤ n
Full source 
@[to_additive IsAddCyclic.card_nsmul_eq_zero_le]
theorem IsCyclic.card_pow_eq_one_le [DecidableEq α] [Fintype α] [IsCyclic α] {n : ℕ} (hn0 : 0 < n) :
    #{a : α | a ^ n = 1} ≤ n :=
  let ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
  calc
    #{a : α | a ^ n = 1} ≤
        #(zpowers (g ^ (Fintype.card α / Nat.gcd n (Fintype.card α))) : Set α).toFinset :=
      card_le_card fun x hx =>
        let ⟨m, hm⟩ := show x ∈ Submonoid.powers g from mem_powers_iff_mem_zpowers.2 <| hg x
        Set.mem_toFinset.2
          ⟨(m / (Fintype.card α / Nat.gcd n (Fintype.card α)) : ℕ), by
            dsimp at hm
            have hgmn : g ^ (m * Nat.gcd n (Fintype.card α)) = 1 := by
              rw [pow_mul, hm, ← pow_gcd_card_eq_one_iff]; exact (mem_filter.1 hx).2
            dsimp only
            rw [zpow_natCast, ← pow_mul, Nat.mul_div_cancel_left', hm]
            refine Nat.dvd_of_mul_dvd_mul_right (gcd_pos_of_pos_left (Fintype.card α) hn0) ?_
            conv_lhs =>
              rw [Nat.div_mul_cancel (Nat.gcd_dvd_right _ _), ← Nat.card_eq_fintype_card,
                ← orderOf_eq_card_of_forall_mem_zpowers hg]
            exact orderOf_dvd_of_pow_eq_one hgmn⟩
    _ ≤ n := by
      let ⟨m, hm⟩ := Nat.gcd_dvd_right n (Fintype.card α)
      have hm0 : 0 < m :=
        Nat.pos_of_ne_zero fun hm0 => by
          rw [hm0, mul_zero, Fintype.card_eq_zero_iff] at hm
          exact hm.elim' 1
      simp only [Set.toFinset_card, SetLike.coe_sort_coe]
      rw [Fintype.card_zpowers, orderOf_pow g, orderOf_eq_card_of_forall_mem_zpowers hg,
        Nat.card_eq_fintype_card]
      nth_rw 2 [hm]; nth_rw 3 [hm]
      rw [Nat.mul_div_cancel_left _ (gcd_pos_of_pos_left _ hn0), gcd_mul_left_left, hm,
        Nat.mul_div_cancel _ hm0]
      exact le_of_dvd hn0 (Nat.gcd_dvd_left _ _)
Upper Bound on Roots of Unity in Finite Cyclic Groups: $|\{a \in G \mid a^n = 1\}| \leq n$
Informal description
Let $\alpha$ be a finite cyclic group with a decidable equality. For any positive integer $n$, the number of elements $a \in \alpha$ satisfying $a^n = 1$ is at most $n$. In other words, $|\{a \in \alpha \mid a^n = 1\}| \leq n$.
IsCyclic.exists_monoid_generator theorem
[Finite α] [IsCyclic α] : ∃ x : α, ∀ y : α, y ∈ Submonoid.powers x
Full source 
@[to_additive]
theorem IsCyclic.exists_monoid_generator [Finite α] [IsCyclic α] :
    ∃ x : α, ∀ y : α, y ∈ Submonoid.powers x := by
  simp_rw [mem_powers_iff_mem_zpowers]
  exact IsCyclic.exists_generator
Existence of a Monoid Generator for Finite Cyclic Groups
Informal description
For any finite cyclic group $\alpha$, there exists an element $x \in \alpha$ such that every element $y \in \alpha$ can be expressed as $x^n$ for some natural number $n$. In other words, $\alpha$ is generated by $x$ as a monoid.
IsCyclic.exists_ofOrder_eq_natCard theorem
[h : IsCyclic α] : ∃ g : α, orderOf g = Nat.card α
Full source 
@[to_additive]
lemma IsCyclic.exists_ofOrder_eq_natCard [h : IsCyclic α] : ∃ g : α, orderOf g = Nat.card α := by
  obtain ⟨g, hg⟩ := h.exists_generator
  use g
  rw [← card_zpowers g, (eq_top_iff' (zpowers g)).mpr hg]
  exact Nat.card_congr (Equiv.Set.univ α)
Existence of an Element with Order Equal to Group Cardinality in Cyclic Groups
Informal description
For any cyclic group $\alpha$, there exists an element $g \in \alpha$ whose order equals the cardinality of $\alpha$ as a natural number, i.e., $\text{orderOf}(g) = \text{Nat.card}(\alpha)$.
MulDistribMulAction.toMonoidHomZModOfIsCyclic definition
(M : Type*) [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) : M →* ZMod n
Full source 
/-- A distributive action of a monoid on a finite cyclic group of order `n` factors through an
action on `ZMod n`. -/
noncomputable def MulDistribMulAction.toMonoidHomZModOfIsCyclic (M : Type*) [Monoid M]
    [IsCyclic G] [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) : M →* ZMod n where
  toFun m := (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose
  map_one' := by
    obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)
    rw [← Int.cast_one, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_one, ← (MulDistribMulAction.toMonoidHom G 1).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, one_smul]
  map_mul' m n := by
    obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := G)
    rw [← Int.cast_mul, ZMod.intCast_eq_intCast_iff, ← hn, ← hg, ← zpow_eq_zpow_iff_modEq,
      zpow_mul', ← (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G n).map_cyclic.choose_spec,
      ← (MulDistribMulAction.toMonoidHom G (m * n)).map_cyclic.choose_spec,
      MulDistribMulAction.toMonoidHom_apply, MulDistribMulAction.toMonoidHom_apply,
      MulDistribMulAction.toMonoidHom_apply, mul_smul]
Factorization of distributive monoid actions on finite cyclic groups via $\mathbb{Z}/n\mathbb{Z}$
Informal description
Given a monoid $M$ acting distributively on a finite cyclic group $G$ of order $n$, there exists a monoid homomorphism from $M$ to the integers modulo $n$ that factors the action. Specifically, for each $m \in M$, the action of $m$ on $G$ corresponds to exponentiation by an integer modulo $n$.
MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply theorem
{M : Type*} [Monoid M] [IsCyclic G] [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) (m : M) (g : G) (k : ℤ) (h : toMonoidHomZModOfIsCyclic G M hn m = k) : m • g = g ^ k
Full source 
theorem MulDistribMulAction.toMonoidHomZModOfIsCyclic_apply {M : Type*} [Monoid M] [IsCyclic G]
    [MulDistribMulAction M G] {n : ℕ} (hn : Nat.card G = n) (m : M) (g : G) (k : ℤ)
    (h : toMonoidHomZModOfIsCyclic G M hn m = k) : m • g = g ^ k := by
  rw [← MulDistribMulAction.toMonoidHom_apply,
    (MulDistribMulAction.toMonoidHom G m).map_cyclic.choose_spec g, zpow_eq_zpow_iff_modEq]
  apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr (orderOf_dvd_natCard g))
  rwa [hn, ← ZMod.intCast_eq_intCast_iff]
Action Characterization for Finite Cyclic Groups via $\mathbb{Z}/n\mathbb{Z}$ Homomorphism
Informal description
Let $G$ be a finite cyclic group of order $n$ with a multiplicative distributive action by a monoid $M$. For any $m \in M$, if the monoid homomorphism $\varphi \colon M \to \mathbb{Z}/n\mathbb{Z}$ satisfies $\varphi(m) = k \pmod{n}$, then the action of $m$ on any element $g \in G$ is given by $m \cdot g = g^k$.
IsCyclic.unique_zpow_zmod theorem
(ha : ∀ x : α, x ∈ zpowers a) (x : α) : ∃! n : ZMod (Fintype.card α), x = a ^ n.val
Full source 
@[to_additive]
theorem IsCyclic.unique_zpow_zmod (ha : ∀ x : α, x ∈ zpowers a) (x : α) :
    ∃! n : ZMod (Fintype.card α), x = a ^ n.val := by
  obtain ⟨n, rfl⟩ := ha x
  refine ⟨n, (?_ : a ^ n = _), fun y (hy : a ^ n = _) ↦ ?_⟩
  · rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Int.modEq_comm, Int.modEq_iff_add_fac, Nat.card_eq_fintype_card, ← ZMod.intCast_eq_iff]
  · rw [← zpow_natCast, zpow_eq_zpow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers ha,
      Nat.card_eq_fintype_card, ← ZMod.intCast_eq_intCast_iff] at hy
    simp [hy]
Unique Existence of Power Representation in Finite Cyclic Groups
Informal description
Let $G$ be a finite cyclic group with generator $a$, meaning every element $x \in G$ can be written as $x = a^n$ for some integer $n$. Then for any element $x \in G$, there exists a unique integer $n$ modulo the order of $G$ (i.e., $n \in \mathbb{Z}/|G|\mathbb{Z}$) such that $x = a^n$.
IsCyclic.image_range_orderOf theorem
(ha : ∀ x : α, x ∈ zpowers a) : Finset.image (fun i => a ^ i) (range (orderOf a)) = univ
Full source 
@[to_additive]
theorem IsCyclic.image_range_orderOf (ha : ∀ x : α, x ∈ zpowers a) :
    Finset.image (fun i => a ^ i) (range (orderOf a)) = univ := by
  simp_rw [← SetLike.mem_coe] at ha
  simp only [_root_.image_range_orderOf, Set.eq_univ_iff_forall.mpr ha, Set.toFinset_univ]
Image of Power Map on Order Range Equals Entire Cyclic Group
Informal description
Let $G$ be a finite cyclic group with generator $a$, meaning every element $x \in G$ can be written as $x = a^n$ for some integer $n$. Then the image of the set $\{0, \ldots, \text{orderOf}(a) - 1\}$ under the power map $i \mapsto a^i$ is equal to the entire group $G$.
IsCyclic.image_range_card theorem
(ha : ∀ x : α, x ∈ zpowers a) : Finset.image (fun i => a ^ i) (range (Nat.card α)) = univ
Full source 
@[to_additive]
theorem IsCyclic.image_range_card (ha : ∀ x : α, x ∈ zpowers a) :
    Finset.image (fun i => a ^ i) (range (Nat.card α)) = univ := by
  rw [← orderOf_eq_card_of_forall_mem_zpowers ha, IsCyclic.image_range_orderOf ha]
Image of Power Map on Cardinality Range Equals Entire Cyclic Group
Informal description
Let $G$ be a finite cyclic group with generator $a$, meaning every element $x \in G$ can be written as $x = a^n$ for some integer $n$. Then the image of the set $\{0, \ldots, |G| - 1\}$ under the power map $i \mapsto a^i$ is equal to the entire group $G$, where $|G|$ denotes the cardinality of $G$.
IsCyclic.ext theorem
[Finite G] [IsCyclic G] {d : ℕ} {a b : ZMod d} (hGcard : Nat.card G = d) (h : ∀ t : G, t ^ a.val = t ^ b.val) : a = b
Full source 
@[to_additive]
lemma IsCyclic.ext [Finite G] [IsCyclic G] {d : ℕ} {a b : ZMod d}
    (hGcard : Nat.card G = d) (h : ∀ t : G, t ^ a.val = t ^ b.val) : a = b := by
  have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := G)
  specialize h g
  subst hGcard
  rw [pow_eq_pow_iff_modEq, orderOf_eq_card_of_forall_mem_zpowers hg,
    ← ZMod.natCast_eq_natCast_iff] at h
  simpa [ZMod.natCast_val, ZMod.cast_id'] using h
Uniqueness of Exponents in Finite Cyclic Groups
Informal description
Let $G$ be a finite cyclic group with cardinality $d$, and let $a, b$ be elements of $\mathbb{Z}/d\mathbb{Z}$. If for every element $t \in G$ we have $t^{a} = t^{b}$ (where $a$ and $b$ are interpreted as integers via their canonical representatives), then $a = b$ in $\mathbb{Z}/d\mathbb{Z}$.
card_orderOf_eq_totient_aux₂ theorem
{d : ℕ} (hd : d ∣ Fintype.card α) : #{a : α | orderOf a = d} = φ d
Full source 
@[to_additive]
theorem card_orderOf_eq_totient_aux₂ {d : ℕ} (hd : d ∣ Fintype.card α) :
    #{a : α | orderOf a = d} = φ d := by
  let c := Fintype.card α
  have hc0 : 0 < c := Fintype.card_pos_iff.2 ⟨1⟩
  apply card_orderOf_eq_totient_aux₁ hn hd
  by_contra h0
  -- Must qualify `Finset.card_eq_zero` because of https://github.com/leanprover/lean4/issues/2849
  simp_rw [not_lt, Nat.le_zero, Finset.card_eq_zero] at h0
  apply lt_irrefl c
  calc
    c = ∑ m ∈ c.divisors, #{a : α | orderOf a = m} := by
      simp only [sum_card_orderOf_eq_card_pow_eq_one hc0.ne']
      apply congr_arg card
      simp [c]
    _ = ∑ m ∈ c.divisors.erase d, #{a : α | orderOf a = m} := by
      rw [eq_comm]
      refine sum_subset (erase_subset _ _) fun m hm₁ hm₂ => ?_
      have : m = d := by
        contrapose! hm₂
        exact mem_erase_of_ne_of_mem hm₂ hm₁
      simp [this, h0]
    _ ≤ ∑ m ∈ c.divisors.erase d, φ m := by
      refine sum_le_sum fun m hm => ?_
      have hmc : m ∣ c := by
        simp only [mem_erase, mem_divisors] at hm
        tauto
      obtain h1 | h1 := (#{a : α | orderOf a = m}).eq_zero_or_pos
      · simp [h1]
      · simp [card_orderOf_eq_totient_aux₁ hn hmc h1]
    _ < ∑ m ∈ c.divisors, φ m :=
      sum_erase_lt_of_pos (mem_divisors.2 ⟨hd, hc0.ne'⟩) (totient_pos.2 (pos_of_dvd_of_pos hd hc0))
    _ = c := sum_totient _
Count of Elements by Order in Finite Groups Equals Euler's Totient Function
Informal description
Let $G$ be a finite group and $d$ a natural number dividing the order of $G$. Then the number of elements in $G$ whose order equals $d$ is given by Euler's totient function $\varphi(d)$.
isCyclic_of_card_pow_eq_one_le theorem
: IsCyclic α
Full source 
@[to_additive isAddCyclic_of_card_nsmul_eq_zero_le, stacks 09HX "This theorem is stronger than \
09HX. It removes the abelian condition, and requires only `≤` instead of `=`."]
theorem isCyclic_of_card_pow_eq_one_le : IsCyclic α :=
  have : Finset.Nonempty {a : α | orderOf a = Nat.card α} :=
    card_pos.1 <| by
      rw [Nat.card_eq_fintype_card, card_orderOf_eq_totient_aux₂ hn dvd_rfl, totient_pos]
      apply Fintype.card_pos
  let ⟨x, hx⟩ := this
  isCyclic_of_orderOf_eq_card x (Finset.mem_filter.1 hx).2
Finite Group is Cyclic if Element Count Condition Holds
Informal description
Let $G$ be a finite group. If for every natural number $d$ dividing the order of $G$, the number of elements $x \in G$ satisfying $x^d = 1$ is at most $d$, then $G$ is cyclic.
IsCyclic.card_orderOf_eq_totient theorem
[IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) : #{a : α | orderOf a = d} = totient d
Full source 
@[to_additive]
lemma IsCyclic.card_orderOf_eq_totient [IsCyclic α] [Fintype α] {d : ℕ} (hd : d ∣ Fintype.card α) :
    #{a : α | orderOf a = d} = totient d := by
  classical apply card_orderOf_eq_totient_aux₂ (fun n => IsCyclic.card_pow_eq_one_le) hd
Count of Elements by Order in Cyclic Groups Equals Euler's Totient Function
Informal description
Let $G$ be a finite cyclic group and $d$ a natural number dividing the order of $G$. Then the number of elements in $G$ with order exactly $d$ equals Euler's totient function $\varphi(d)$. In other words: $$|\{g \in G \mid \text{orderOf}(g) = d\}| = \varphi(d)$$
isSimpleGroup_of_prime_card theorem
{p : ℕ} [hp : Fact p.Prime] (h : Nat.card α = p) : IsSimpleGroup α
Full source 
/-- A finite group of prime order is simple. -/
@[to_additive "A finite group of prime order is simple."]
theorem isSimpleGroup_of_prime_card {p : ℕ} [hp : Fact p.Prime]
    (h : Nat.card α = p) : IsSimpleGroup α := by
  subst h
  have : Finite α := Nat.finite_of_card_ne_zero hp.1.ne_zero
  have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp hp.1.one_lt
  exact ⟨fun H _ => H.eq_bot_or_eq_top_of_prime_card⟩
Finite Groups of Prime Order are Simple
Informal description
Let $G$ be a finite group of order $p$, where $p$ is a prime number. Then $G$ is a simple group.
commutative_of_cyclic_center_quotient theorem
[IsCyclic G'] (f : G →* G') (hf : f.ker ≤ center G) (a b : G) : a * b = b * a
Full source 
/-- A group is commutative if the quotient by the center is cyclic.
  Also see `commGroupOfCyclicCenterQuotient` for the `CommGroup` instance. -/
@[to_additive
      "A group is commutative if the quotient by the center is cyclic.
      Also see `addCommGroupOfCyclicCenterQuotient` for the `AddCommGroup` instance."]
theorem commutative_of_cyclic_center_quotient [IsCyclic G'] (f : G →* G') (hf : f.ker ≤ center G)
    (a b : G) : a * b = b * a :=
  let ⟨⟨x, y, (hxy : f y = x)⟩, (hx : ∀ a : f.range, a ∈ zpowers _)⟩ :=
    IsCyclic.exists_generator (α := f.range)
  let ⟨m, hm⟩ := hx ⟨f a, a, rfl⟩
  let ⟨n, hn⟩ := hx ⟨f b, b, rfl⟩
  have hm : x ^ m = f a := by simpa [Subtype.ext_iff] using hm
  have hn : x ^ n = f b := by simpa [Subtype.ext_iff] using hn
  have ha : y ^ (-m) * a ∈ center G :=
    hf (by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x m, hm, inv_mul_cancel])
  have hb : y ^ (-n) * b ∈ center G :=
    hf (by rw [f.mem_ker, f.map_mul, f.map_zpow, hxy, zpow_neg x n, hn, inv_mul_cancel])
  calc
    a * b = y ^ m * (y ^ (-m) * a * y ^ n) * (y ^ (-n) * b) := by simp [mul_assoc]
    _ = y ^ m * (y ^ n * (y ^ (-m) * a)) * (y ^ (-n) * b) := by rw [mem_center_iff.1 ha]
    _ = y ^ m * y ^ n * y ^ (-m) * (a * (y ^ (-n) * b)) := by simp [mul_assoc]
    _ = y ^ m * y ^ n * y ^ (-m) * (y ^ (-n) * b * a) := by rw [mem_center_iff.1 hb]
    _ = b * a := by group
Commutativity from Cyclic Quotient with Central Kernel
Informal description
Let $G$ and $G'$ be groups with a group homomorphism $f \colon G \to G'$. If $G'$ is cyclic and the kernel of $f$ is contained in the center of $G$, then $G$ is commutative. That is, for any elements $a, b \in G$, we have $a \cdot b = b \cdot a$.
commGroupOfCyclicCenterQuotient definition
[IsCyclic G'] (f : G →* G') (hf : f.ker ≤ center G) : CommGroup G
Full source 
/-- A group is commutative if the quotient by the center is cyclic. -/
@[to_additive
      "A group is commutative if the quotient by the center is cyclic."]
def commGroupOfCyclicCenterQuotient [IsCyclic G'] (f : G →* G') (hf : f.ker ≤ center G) :
    CommGroup G :=
  { show Group G by infer_instance with mul_comm := commutative_of_cyclic_center_quotient f hf }
Commutative group structure from cyclic center quotient
Informal description
Given a group homomorphism $f \colon G \to G'$ where $G'$ is a cyclic group and the kernel of $f$ is contained in the center of $G$, the group $G$ can be endowed with a commutative group structure. The commutativity follows from the condition that the quotient of $G$ by the kernel of $f$ (which is cyclic) implies that $G$ itself is commutative.
IsSimpleGroup.prime_card theorem
[Finite α] : (Nat.card α).Prime
Full source 
@[to_additive]
theorem prime_card [Finite α] : (Nat.card α).Prime := by
  have h0 : 0 < Nat.card α := Nat.card_pos
  obtain ⟨g, hg⟩ := IsCyclic.exists_generator (α := α)
  rw [Nat.prime_def]
  refine ⟨Finite.one_lt_card_iff_nontrivial.2 inferInstance, fun n hn => ?_⟩
  refine (IsSimpleOrder.eq_bot_or_eq_top (Subgroup.zpowers (g ^ n))).symm.imp ?_ ?_
  · intro h
    have hgo := orderOf_pow (n := n) g
    rw [orderOf_eq_card_of_forall_mem_zpowers hg, Nat.gcd_eq_right_iff_dvd.2 hn,
      orderOf_eq_card_of_forall_mem_zpowers, eq_comm,
      Nat.div_eq_iff_eq_mul_left (Nat.pos_of_dvd_of_pos hn h0) hn] at hgo
    · exact (mul_left_cancel₀ (ne_of_gt h0) ((mul_one (Nat.card α)).trans hgo)).symm
    · intro x
      rw [h]
      exact Subgroup.mem_top _
  · intro h
    apply le_antisymm (Nat.le_of_dvd h0 hn)
    rw [← orderOf_eq_card_of_forall_mem_zpowers hg]
    apply orderOf_le_of_pow_eq_one (Nat.pos_of_dvd_of_pos hn h0)
    rw [← Subgroup.mem_bot, ← h]
    exact Subgroup.mem_zpowers _
Cardinality of Finite Simple Commutative Groups is Prime
Informal description
For any finite simple commutative group $\alpha$, the cardinality of $\alpha$ is a prime number.
CommGroup.is_simple_iff_isCyclic_and_prime_card theorem
[Finite α] [CommGroup α] : IsSimpleGroup α ↔ IsCyclic α ∧ (Nat.card α).Prime
Full source 
@[to_additive]
theorem CommGroup.is_simple_iff_isCyclic_and_prime_card [Finite α] [CommGroup α] :
    IsSimpleGroupIsSimpleGroup α ↔ IsCyclic α ∧ (Nat.card α).Prime := by
  constructor
  · intro h
    exact ⟨IsSimpleGroup.isCyclic, IsSimpleGroup.prime_card⟩
  · rintro ⟨_, hp⟩
    haveI : Fact (Nat.card α).Prime := ⟨hp⟩
    exact isSimpleGroup_of_prime_card rfl
Characterization of Finite Simple Commutative Groups: Cyclic with Prime Order
Informal description
Let $G$ be a finite commutative group. Then $G$ is simple if and only if $G$ is cyclic and its order is a prime number.
IsCyclic.exponent_eq_card theorem
[Group α] [IsCyclic α] : exponent α = Nat.card α
Full source 
@[to_additive]
theorem IsCyclic.exponent_eq_card [Group α] [IsCyclic α] :
    exponent α = Nat.card α := by
  obtain ⟨g, hg⟩ := IsCyclic.exists_ofOrder_eq_natCard (α := α)
  apply Nat.dvd_antisymm Group.exponent_dvd_nat_card
  rw [← hg]
  exact order_dvd_exponent _
Exponent Equals Cardinality in Cyclic Groups
Informal description
For any cyclic group $\alpha$, the exponent of $\alpha$ is equal to the cardinality of $\alpha$ as a natural number, i.e., $\text{exponent}(\alpha) = \text{Nat.card}(\alpha)$.
IsCyclic.of_exponent_eq_card theorem
[CommGroup α] [Finite α] (h : exponent α = Nat.card α) : IsCyclic α
Full source 
@[to_additive]
theorem IsCyclic.of_exponent_eq_card [CommGroup α] [Finite α] (h : exponent α = Nat.card α) :
    IsCyclic α :=
  let ⟨_⟩ := nonempty_fintype α
  let ⟨g, _, hg⟩ := Finset.mem_image.mp (Finset.max'_mem _ _)
  isCyclic_of_orderOf_eq_card g <| hg.trans <| exponent_eq_max'_orderOf.symm.trans h
Finite Commutative Group is Cyclic When Exponent Equals Cardinality
Informal description
Let $G$ be a finite commutative group. If the exponent of $G$ (the least common multiple of the orders of all elements of $G$) is equal to the cardinality of $G$, then $G$ is cyclic.
IsCyclic.iff_exponent_eq_card theorem
[CommGroup α] [Finite α] : IsCyclic α ↔ exponent α = Nat.card α
Full source 
@[to_additive]
theorem IsCyclic.iff_exponent_eq_card [CommGroup α] [Finite α] :
    IsCyclicIsCyclic α ↔ exponent α = Nat.card α :=
  ⟨fun _ => IsCyclic.exponent_eq_card, IsCyclic.of_exponent_eq_card⟩
Characterization of Finite Cyclic Commutative Groups via Exponent and Cardinality
Informal description
For a finite commutative group $G$, the group $G$ is cyclic if and only if its exponent (the least common multiple of the orders of all elements of $G$) is equal to the cardinality of $G$.
IsCyclic.exponent_eq_zero_of_infinite theorem
[Group α] [IsCyclic α] [Infinite α] : exponent α = 0
Full source 
@[to_additive]
theorem IsCyclic.exponent_eq_zero_of_infinite [Group α] [IsCyclic α] [Infinite α] :
    exponent α = 0 :=
  let ⟨_, hg⟩ := IsCyclic.exists_generator (α := α)
  exponent_eq_zero_of_order_zero <| Infinite.orderOf_eq_zero_of_forall_mem_zpowers hg
Exponent of Infinite Cyclic Group is Zero
Informal description
For any infinite cyclic group $\alpha$, the exponent of $\alpha$ is zero.
not_isCyclic_iff_exponent_eq_prime theorem
[Group α] {p : ℕ} (hp : p.Prime) (hα : Nat.card α = p ^ 2) : ¬IsCyclic α ↔ Monoid.exponent α = p
Full source 
/-- A group of order `p ^ 2` is not cyclic if and only if its exponent is `p`. -/
@[to_additive]
lemma not_isCyclic_iff_exponent_eq_prime [Group α] {p : ℕ} (hp : p.Prime)
    (hα : Nat.card α = p ^ 2) : ¬ IsCyclic α¬ IsCyclic α ↔ Monoid.exponent α = p := by
  -- G is a nontrivial fintype of cardinality `p ^ 2`
  have : Finite α := Nat.finite_of_card_ne_zero (hα ▸ pow_ne_zero 2 hp.ne_zero)
  have : Nontrivial α := Finite.one_lt_card_iff_nontrivial.mp
    (hα ▸ one_lt_pow₀ hp.one_lt two_ne_zero)
  /- in the forward direction, we apply `exponent_eq_prime_iff`, and the reverse direction follows
  immediately because if `α` has exponent `p`, it has no element of order `p ^ 2`. -/
  refine ⟨fun h_cyc ↦ (Monoid.exponent_eq_prime_iff hp).mpr fun g hg ↦ ?_, fun h_exp h_cyc ↦ by
    obtain (rfl|rfl) := eq_zero_or_one_of_sq_eq_self <| hα ▸ h_exp ▸ (h_cyc.exponent_eq_card).symm
    · exact Nat.not_prime_zero hp
    · exact Nat.not_prime_one hp⟩
  /- we must show every non-identity element has order `p`. By Lagrange's theorem, the only possible
  orders of `g` are `1`, `p`, or `p ^ 2`. It can't be the former because `g ≠ 1`, and it can't
  the latter because the group isn't cyclic. -/
  have := (Nat.mem_divisors (m := p ^ 2)).mpr ⟨hα ▸ orderOf_dvd_natCard (x := g), by aesop⟩
  simp? [Nat.divisors_prime_pow hp 2] at this says
    simp only [Nat.divisors_prime_pow hp 2, Nat.reduceAdd, Finset.mem_map, Finset.mem_range,
      Function.Embedding.coeFn_mk] at this
  obtain ⟨a, ha, ha'⟩ := this
  interval_cases a
  · exact False.elim <| hg <| orderOf_eq_one_iff.mp <| by aesop
  · aesop
  · exact False.elim <| h_cyc <| isCyclic_of_orderOf_eq_card g <| by aesop
Non-cyclic group of order $p^2$ has exponent $p$
Informal description
Let $\alpha$ be a finite group of order $p^2$ where $p$ is a prime number. Then $\alpha$ is not cyclic if and only if the exponent of $\alpha$ is equal to $p$.
zmultiplesHom_ker_eq theorem
[AddGroup G] (g : G) : (zmultiplesHom G g).ker = zmultiples ↑(addOrderOf g)
Full source 
/-- The kernel of `zmultiplesHom G g` is equal to the additive subgroup generated by
    `addOrderOf g`. -/
theorem zmultiplesHom_ker_eq [AddGroup G] (g : G) :
    (zmultiplesHom G g).ker = zmultiples ↑(addOrderOf g) := by
  ext
  simp_rw [AddMonoidHom.mem_ker, mem_zmultiples_iff, zmultiplesHom_apply,
    ← addOrderOf_dvd_iff_zsmul_eq_zero, zsmul_eq_mul', Int.cast_id, dvd_def, eq_comm]
Kernel of `zmultiplesHom` Equals Subgroup Generated by Additive Order
Informal description
Let $G$ be an additive group and $g \in G$. The kernel of the homomorphism `zmultiplesHom G g` is equal to the additive subgroup generated by the additive order of $g$, i.e., \[ \text{ker}(zmultiplesHom G g) = \langle \text{addOrderOf } g \rangle. \]
zpowersHom_ker_eq theorem
[Group G] (g : G) : (zpowersHom G g).ker = zpowers (Multiplicative.ofAdd ↑(orderOf g))
Full source 
/-- The kernel of `zpowersHom G g` is equal to the subgroup generated by `orderOf g`. -/
theorem zpowersHom_ker_eq [Group G] (g : G) :
    (zpowersHom G g).ker = zpowers (Multiplicative.ofAdd ↑(orderOf g)) :=
  congr_arg AddSubgroup.toSubgroup <| zmultiplesHom_ker_eq (Additive.ofMul g)
Kernel of `zpowersHom` Equals Subgroup Generated by Order of Element
Informal description
Let $G$ be a group and $g \in G$. The kernel of the homomorphism `zpowersHom G g` is equal to the subgroup generated by the multiplicative order of $g$, i.e., \[ \text{ker}(\text{zpowersHom } G \ g) = \langle g^{\text{orderOf } g} \rangle. \]
zmodAddCyclicAddEquiv definition
[AddGroup G] (h : IsAddCyclic G) : ZMod (Nat.card G) ≃+ G
Full source 
/-- The isomorphism from `ZMod n` to any cyclic additive group of `Nat.card` equal to `n`. -/
noncomputable def zmodAddCyclicAddEquiv [AddGroup G] (h : IsAddCyclic G) :
    ZModZMod (Nat.card G) ≃+ G := by
  let n := Nat.card G
  let ⟨g, surj⟩ := Classical.indefiniteDescription _ h.exists_generator
  have kereq : ((zmultiplesHom G) g).ker = zmultiples ↑(Nat.card G) := by
    rw [zmultiplesHom_ker_eq]
    congr
    rw [← Nat.card_zmultiples]
    exact Nat.card_congr (Equiv.subtypeUnivEquiv surj)
  exact Int.quotientZMultiplesNatEquivZMod n
    |>.symm.trans <| QuotientAddGroup.quotientAddEquivOfEq kereq
    |>.symm.trans <| QuotientAddGroup.quotientKerEquivOfSurjective (zmultiplesHom G g) surj
Isomorphism between \( \mathbb{Z}/n\mathbb{Z} \) and a cyclic additive group of order \( n \)
Informal description
Given an additive group \( G \) that is cyclic (i.e., there exists an element \( g \in G \) such that every element of \( G \) can be written as \( n \cdot g \) for some integer \( n \)), there is an additive isomorphism between the additive group \( \mathbb{Z}/n\mathbb{Z} \) (where \( n \) is the cardinality of \( G \)) and \( G \). More precisely, the isomorphism is constructed as follows: 1. Identify a generator \( g \) of \( G \). 2. Show that the kernel of the homomorphism \( \mathbb{Z} \to G \) sending \( k \) to \( k \cdot g \) is the subgroup \( n\mathbb{Z} \). 3. Use this to construct an isomorphism \( \mathbb{Z}/n\mathbb{Z} \cong G \).
zmodCyclicMulEquiv definition
[Group G] (h : IsCyclic G) : Multiplicative (ZMod (Nat.card G)) ≃* G
Full source 
/-- The isomorphism from `Multiplicative (ZMod n)` to any cyclic group of `Nat.card` equal to `n`.
-/
noncomputable def zmodCyclicMulEquiv [Group G] (h : IsCyclic G) :
    MultiplicativeMultiplicative (ZMod (Nat.card G)) ≃* G :=
  AddEquiv.toMultiplicative <| zmodAddCyclicAddEquiv <| isAddCyclic_additive_iff.2 h
Isomorphism between \( \mathbb{Z}/n\mathbb{Z} \) and a cyclic group of order \( n \)
Informal description
Given a cyclic group \( G \) (i.e., a group generated by a single element), there is a multiplicative isomorphism between the multiplicative version of the integers modulo \( n \) (where \( n \) is the cardinality of \( G \)) and \( G \). More precisely, the isomorphism is constructed as follows: 1. Convert the cyclic group \( G \) to its additive counterpart using the additive equivalence. 2. Apply the isomorphism between \( \mathbb{Z}/n\mathbb{Z} \) and the additive cyclic group. 3. Convert the result back to a multiplicative isomorphism.
addEquivOfAddCyclicCardEq definition
[AddGroup G] [AddGroup G'] [hG : IsAddCyclic G] [hH : IsAddCyclic G'] (hcard : Nat.card G = Nat.card G') : G ≃+ G'
Full source 
/-- Two cyclic additive groups of the same cardinality are isomorphic. -/
noncomputable def addEquivOfAddCyclicCardEq [AddGroup G] [AddGroup G'] [hG : IsAddCyclic G]
    [hH : IsAddCyclic G'] (hcard : Nat.card G = Nat.card G') : G ≃+ G' := hcard ▸
  zmodAddCyclicAddEquiv hG |>.symm.trans (zmodAddCyclicAddEquiv hH)
Isomorphism between cyclic additive groups of the same order
Informal description
Given two cyclic additive groups \( G \) and \( G' \) with the same cardinality, there exists an additive isomorphism between them. More precisely, if \( G \) and \( G' \) are both cyclic additive groups and \( \text{card}(G) = \text{card}(G') \), then there exists a bijective additive homomorphism \( G \simeq G' \).
mulEquivOfCyclicCardEq definition
[Group G] [Group G'] [hG : IsCyclic G] [hH : IsCyclic G'] (hcard : Nat.card G = Nat.card G') : G ≃* G'
Full source 
/-- Two cyclic groups of the same cardinality are isomorphic. -/
@[to_additive existing]
noncomputable def mulEquivOfCyclicCardEq [Group G] [Group G'] [hG : IsCyclic G]
    [hH : IsCyclic G'] (hcard : Nat.card G = Nat.card G') : G ≃* G' := hcard ▸
  zmodCyclicMulEquiv hG |>.symm.trans (zmodCyclicMulEquiv hH)
Isomorphism between cyclic groups of the same order
Informal description
Given two cyclic groups \( G \) and \( G' \) with the same cardinality, there exists a multiplicative isomorphism between them. More precisely, if \( G \) and \( G' \) are both cyclic groups and \( \text{card}(G) = \text{card}(G') \), then there exists a bijective multiplicative homomorphism \( G \simeq^* G' \).
mulEquivOfPrimeCardEq definition
{p : ℕ} [Group G] [Group G'] [Fact p.Prime] (hG : Nat.card G = p) (hH : Nat.card G' = p) : G ≃* G'
Full source 
/-- Two groups of the same prime cardinality are isomorphic. -/
@[to_additive "Two additive groups of the same prime cardinality are isomorphic."]
noncomputable def mulEquivOfPrimeCardEq {p : ℕ} [Group G] [Group G']
    [Fact p.Prime] (hG : Nat.card G = p) (hH : Nat.card G' = p) : G ≃* G' := by
  have hGcyc := isCyclic_of_prime_card hG
  have hHcyc := isCyclic_of_prime_card hH
  apply mulEquivOfCyclicCardEq
  exact hG.trans hH.symm
Isomorphism between groups of the same prime order
Informal description
Given two groups \( G \) and \( G' \) of the same prime order \( p \), there exists a multiplicative isomorphism between them. More precisely, if \( G \) and \( G' \) are groups with \( \text{card}(G) = \text{card}(G') = p \) for some prime \( p \), then there exists a bijective multiplicative homomorphism \( G \simeq^* G' \).
IsCyclic.mulAutMulEquiv definition
[Group G] [h : IsCyclic G] : MulAut G ≃* (ZMod (Nat.card G))ˣ
Full source 
/-- The automorphism group of a cyclic group is isomorphic to the multiplicative group of ZMod. -/
@[simps!]
noncomputable def IsCyclic.mulAutMulEquiv [Group G] [h : IsCyclic G] :
    MulAutMulAut G ≃* (ZMod (Nat.card G))ˣ :=
  ((MulAut.congr (zmodCyclicMulEquiv h)).symm.trans
    (MulAutMultiplicative (ZMod (Nat.card G)))).trans (ZMod.AddAutEquivUnits (Nat.card G))
Isomorphism between automorphism group of a cyclic group and units of \( \mathbb{Z}/n\mathbb{Z} \)
Informal description
For a cyclic group \( G \), the group of multiplicative automorphisms \( \text{MulAut}(G) \) is isomorphic to the group of units \( (\mathbb{Z}/n\mathbb{Z})^\times \), where \( n \) is the cardinality of \( G \). More precisely, the isomorphism is constructed as follows: 1. First, use the isomorphism \( \text{Multiplicative}(\mathbb{Z}/n\mathbb{Z}) \simeq^* G \) provided by `zmodCyclicMulEquiv`. 2. Then, take the automorphism group of both sides to get \( \text{MulAut}(\text{Multiplicative}(\mathbb{Z}/n\mathbb{Z})) \simeq^* \text{MulAut}(G) \). 3. Finally, identify \( \text{MulAut}(\text{Multiplicative}(\mathbb{Z}/n\mathbb{Z})) \) with the group of additive automorphisms of \( \mathbb{Z}/n\mathbb{Z} \), which is in turn isomorphic to \( (\mathbb{Z}/n\mathbb{Z})^\times \).
IsCyclic.card_mulAut theorem
[Group G] [Finite G] [h : IsCyclic G] : Nat.card (MulAut G) = Nat.totient (Nat.card G)
Full source 
theorem IsCyclic.card_mulAut [Group G] [Finite G] [h : IsCyclic G] :
    Nat.card (MulAut G) = Nat.totient (Nat.card G) := by
  have : NeZero (Nat.card G) := ⟨Nat.card_pos.ne'⟩
  rw [← ZMod.card_units_eq_totient, ← Nat.card_eq_fintype_card]
  exact Nat.card_congr (mulAutMulEquiv G)
Cardinality of Automorphism Group of Finite Cyclic Group Equals Euler's Totient Function
Informal description
For any finite cyclic group $G$, the cardinality of its automorphism group $\mathrm{Aut}(G)$ is equal to Euler's totient function $\varphi(n)$ evaluated at $n = |G|$, the order of $G$.
monoidHomOfForallMemZpowers definition
: G →* G'
Full source 
/-- 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'`. -/
@[to_additive
   "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'`."]
noncomputable
def monoidHomOfForallMemZpowers : G →* G' where
  toFun x := g' ^ (Classical.choose <| mem_zpowers_iff.mp <| hg x)
  map_one' := orderOf_dvd_iff_zpow_eq_one.mp <|
                (Int.natCast_dvd_natCast.mpr hg').trans <| orderOf_dvd_iff_zpow_eq_one.mpr <|
                Classical.choose_spec <| mem_zpowers_iff.mp <| hg 1
  map_mul' x y := by
    simp only [← zpow_add, zpow_eq_zpow_iff_modEq]
    apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
    rw [← zpow_eq_zpow_iff_modEq, zpow_add]
    simp only [fun x ↦ Classical.choose_spec <| mem_zpowers_iff.mp <| hg x]
Group homomorphism defined by generator image
Informal description
Given a group $G$ with a generator $g$ (i.e., every element of $G$ is of the form $g^n$ for some integer $n$), and another group $G'$ with an element $g'$ whose order divides the order of $g$, there exists a group homomorphism $f \colon G \to G'$ such that $f(g) = g'$.
monoidHomOfForallMemZpowers_apply_gen theorem
: monoidHomOfForallMemZpowers hg hg' g = g'
Full source 
@[to_additive (attr := simp)]
lemma monoidHomOfForallMemZpowers_apply_gen :
    monoidHomOfForallMemZpowers hg hg' g = g' := by
  simp only [monoidHomOfForallMemZpowers, MonoidHom.coe_mk, OneHom.coe_mk]
  nth_rw 2 [← zpow_one g']
  rw [zpow_eq_zpow_iff_modEq]
  apply Int.ModEq.of_dvd (Int.natCast_dvd_natCast.mpr hg')
  rw [← zpow_eq_zpow_iff_modEq, zpow_one]
  exact Classical.choose_spec <| mem_zpowers_iff.mp <| hg g
Generator Image Property of Cyclic Group Homomorphism: $f(g) = g'$
Informal description
Let $G$ be a cyclic group with generator $g$, and let $G'$ be another group with an element $g'$ such that the order of $g'$ divides the order of $g$. Then the group homomorphism $f \colon G \to G'$ defined by $f(g^n) = g'^n$ for all integers $n$ satisfies $f(g) = g'$.
mulEquivOfOrderOfEq definition
: G ≃* G'
Full source 
/-- Given two groups that are generated by elements `g` and `g'` of the same order,
we obtain an isomorphism sending `g` to `g'`. -/
@[to_additive
   "Given two additive groups that are generated by elements `g` and `g'` of the same order,
   we obtain an isomorphism sending `g` to `g'`."]
noncomputable
def mulEquivOfOrderOfEq : G ≃* G' := by
  refine MonoidHom.toMulEquiv (monoidHomOfForallMemZpowers hg h.symm.dvd)
    (monoidHomOfForallMemZpowers hg' h.dvd) ?_ ?_ <;>
  refine (MonoidHom.eq_iff_eq_on_generator (by assumption) _ _).mpr ?_ <;>
  simp only [MonoidHom.coe_comp, Function.comp_apply, monoidHomOfForallMemZpowers_apply_gen,
    MonoidHom.id_apply]
Group isomorphism between cyclic groups with generators of equal order
Informal description
Given two groups $G$ and $G'$ with generators $g \in G$ and $g' \in G'$ respectively, where $g$ and $g'$ have the same order, there exists a multiplicative isomorphism (group isomorphism) $\varphi \colon G \to G'$ that maps $g$ to $g'$.
mulEquivOfOrderOfEq_apply_gen theorem
: mulEquivOfOrderOfEq hg hg' h g = g'
Full source 
@[to_additive (attr := simp)]
lemma mulEquivOfOrderOfEq_apply_gen : mulEquivOfOrderOfEq hg hg' h g = g' :=
  monoidHomOfForallMemZpowers_apply_gen hg h.symm.dvd
Generator Image Property of Cyclic Group Isomorphism: $\varphi(g) = g'$
Informal description
Let $G$ and $G'$ be cyclic groups with generators $g \in G$ and $g' \in G'$ respectively, such that $\text{orderOf}(g) = \text{orderOf}(g')$. Then the group isomorphism $\varphi: G \to G'$ defined by $\varphi(g^n) = g'^n$ for all $n \in \mathbb{Z}$ satisfies $\varphi(g) = g'$.
mulEquivOfOrderOfEq_symm theorem
: (mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg h.symm
Full source 
@[to_additive (attr := simp)]
lemma mulEquivOfOrderOfEq_symm :
    (mulEquivOfOrderOfEq hg hg' h).symm = mulEquivOfOrderOfEq hg' hg h.symm := rfl
Inverse of Cyclic Group Isomorphism with Equal Order Generators
Informal description
Let $G$ and $G'$ be cyclic groups with generators $g \in G$ and $g' \in G'$ respectively, such that $\text{orderOf}(g) = \text{orderOf}(g')$. Then the inverse of the group isomorphism $\varphi: G \to G'$ (which maps $g$ to $g'$) is equal to the group isomorphism $\psi: G' \to G$ (which maps $g'$ to $g$).
mulEquivOfOrderOfEq_symm_apply_gen theorem
: (mulEquivOfOrderOfEq hg hg' h).symm g' = g
Full source 
@[to_additive] -- `simp` can prove this by a combination of the two preceding lemmas
lemma mulEquivOfOrderOfEq_symm_apply_gen : (mulEquivOfOrderOfEq hg hg' h).symm g' = g :=
  monoidHomOfForallMemZpowers_apply_gen hg' h.dvd
Inverse Cyclic Group Isomorphism Maps Generator Back
Informal description
Let $G$ and $G'$ be cyclic groups with generators $g \in G$ and $g' \in G'$ respectively, such that $\text{order}(g) = \text{order}(g')$. Then the inverse of the group isomorphism $\varphi \colon G \to G'$ (defined by $\varphi(g) = g'$) satisfies $\varphi^{-1}(g') = g$.