From 0af1e05a81dd7ca5959dd5add272938b5c2af946 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Fri, 14 Aug 2026 08:44:34 +0900
Subject: [PATCH 1/3] first commit

---
 .../Algebra/Group/Subgroup/ZPowers/Basic.lean | 10 ++++
 Mathlib/Data/Nat/Basic.lean                   |  4 ++
 Mathlib/GroupTheory/OrderOfElement.lean       | 14 +++++
 .../GroupTheory/SpecificGroups/Cyclic.lean    | 56 +++++++++++++++++++
 4 files changed, 84 insertions(+)

diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
index 5440c705af0fc6..941d953632235a 100644
--- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Basic.lean
@@ -137,8 +137,18 @@ theorem zpowers_one_eq_bot : Subgroup.zpowers (1 : G) = ⊥ :=
 theorem zpowers_inv : zpowers g⁻¹ = zpowers g :=
   eq_of_forall_ge_iff fun _ ↦ by simp only [zpowers_le, inv_mem_iff]
 
+/-- The subgroup generated by `g * h` is contained in the one generated by `g` and `h`. -/
+@[to_additive /-- The subgroup generated by `g + h` is contained in the one generated by `g`
+and `h`. -/]
+theorem zpowers_mul_le_sup (g h : G) : zpowers (g * h) ≤ zpowers g ⊔ zpowers h :=
+  zpowers_le.mpr (mul_mem_sup (mem_zpowers g) (mem_zpowers h))
+
 end Subgroup
 
+theorem Int.zmultiples_le_zmultiples_iff {a b : ℤ} :
+    AddSubgroup.zmultiples a ≤ AddSubgroup.zmultiples b ↔ b ∣ a := by
+  rw [AddSubgroup.zmultiples_le, Int.mem_zmultiples_iff]
+
 theorem Int.zmultiples_natAbs (a : ℤ) :
     AddSubgroup.zmultiples (a.natAbs : ℤ) = AddSubgroup.zmultiples a := by
   simp [le_antisymm_iff, Int.mem_zmultiples_iff, Int.dvd_natAbs, Int.natAbs_dvd]
diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
index f3999b1119c627..8019798292e80d 100644
--- a/Mathlib/Data/Nat/Basic.lean
+++ b/Mathlib/Data/Nat/Basic.lean
@@ -119,6 +119,10 @@ lemma set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ k : ℕ, k ∈ S 
 
 /-! ### `mod`, `dvd` -/
 
+/-- Two natural numbers dividing each other are equal. -/
+protected lemma dvd_antisymm_iff : m ∣ n ∧ n ∣ m ↔ m = n :=
+  ⟨fun ⟨h₁, h₂⟩ ↦ Nat.dvd_antisymm h₁ h₂, by simp +contextual⟩
+
 /-- `dvd` is injective in the left argument -/
 lemma dvd_left_injective : Function.Injective ((· ∣ ·) : ℕ → ℕ → Prop) := fun _ _ h =>
   dvd_right_iff_eq.mp fun a => iff_of_eq (congr_fun h a)
diff --git a/Mathlib/GroupTheory/OrderOfElement.lean b/Mathlib/GroupTheory/OrderOfElement.lean
index d813d174282025..b30ce48629d408 100644
--- a/Mathlib/GroupTheory/OrderOfElement.lean
+++ b/Mathlib/GroupTheory/OrderOfElement.lean
@@ -1046,6 +1046,15 @@ lemma orderOf_eq_zero_iff_eq_zero {G₀ : Type*} [GroupWithZero G₀] [Finite G
 section FiniteGroup
 variable [Group G] {x y : G}
 
+@[to_additive]
+theorem orderOf_pow_natAbs (x : G) (n : ℤ) : orderOf (x ^ n.natAbs) = orderOf (x ^ n) := by
+  cases n <;> simp
+
+@[to_additive]
+theorem orderOf_zpow' (x : G) {n : ℤ} (h : n ≠ 0) :
+    orderOf (x ^ n) = orderOf x / (orderOf x).gcd n.natAbs := by
+  rw [← orderOf_pow' _ (Int.natAbs_ne_zero.mpr h), orderOf_pow_natAbs]
+
 @[to_additive]
 theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x] := by
   rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]
@@ -1091,6 +1100,11 @@ theorem mem_zpowers_pow_iff {g : G} {k : ℕ} :
 section Finite
 variable [Finite G]
 
+@[to_additive]
+theorem orderOf_zpow (x : G) (n : ℤ) :
+    orderOf (x ^ n) = orderOf x / (orderOf x).gcd n.natAbs := by
+  rw [← orderOf_pow, orderOf_pow_natAbs]
+
 @[to_additive]
 theorem exists_zpow_eq_one (x : G) : ∃ (i : ℤ) (_ : i ≠ 0), x ^ (i : ℤ) = 1 := by
   obtain ⟨w, hw1, hw2⟩ := isOfFinOrder_of_finite x
diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
index f18ede9c228c61..e654aca0a431d2 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -5,6 +5,7 @@ Authors: Johannes Hölzl
 -/
 module
 
+public import Mathlib.Algebra.Group.Subgroup.ZPowers.Lemmas
 public import Mathlib.Algebra.Group.TypeTags.Finite
 public import Mathlib.Algebra.Order.Hom.TypeTags
 public import Mathlib.Data.Nat.Totient
@@ -395,6 +396,61 @@ 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)
 
+/-- `zmultiples (i • g) ≤ zmultiples (j • g)` iff `j.gcd (addOrderOf g) ∣ i.gcd (addOrderOf g)`.
+This characterizes inclusion of cyclic subgroups of an additive group generated by integer
+multiples of a single element. -/
+theorem AddSubgroup.zmultiples_le_zmultiples_iff [AddGroup G] (g : G) (i j : ℤ) :
+    zmultiples (i • g) ≤ zmultiples (j • g) ↔
+      j.gcd (addOrderOf g) ∣ i.gcd (addOrderOf g) := by
+  simp_rw [← zmultiplesHom_apply, ← AddMonoidHom.map_zmultiples,
+    AddSubgroup.map_le_map_iff', zmultiplesHom_ker_eq, Int.zmultiples_sup,
+    Int.zmultiples_le_zmultiples_iff, Int.natCast_dvd_natCast]
+
+@[to_additive existing]
+theorem Subgroup.zpowers_le_zpowers_iff [Group G] (g : G) (i j : ℤ) :
+    zpowers (g ^ i) ≤ zpowers (g ^ j) ↔ j.gcd (orderOf g) ∣ i.gcd (orderOf g) :=
+  AddSubgroup.zmultiples_le_zmultiples_iff (Additive.ofMul g) i j
+
+/-- In an additive group generated by `g`, the index of `zmultiples (i • g)` is the gcd of `i`
+and the order of `g`. -/
+theorem AddSubgroup.index_zmultiples_zsmul [AddGroup G] {g : G} (hg : zmultiples g = ⊤) (i : ℤ) :
+    (zmultiples (i • g)).index = i.gcd (addOrderOf g) := by
+  rw [← zmultiplesHom_apply, ← AddMonoidHom.map_zmultiples, AddSubgroup.index_map,
+    zmultiplesHom_ker_eq, Int.zmultiples_sup, Int.index_zmultiples, range_zmultiplesHom, hg,
+    AddSubgroup.index_top, mul_one, Int.natAbs_natCast]
+
+@[to_additive existing]
+theorem Subgroup.index_zpowers_zpow [Group G] {g : G} (hg : zpowers g = ⊤) (i : ℤ) :
+    (zpowers (g ^ i)).index = i.gcd (orderOf g) := by
+  refine AddSubgroup.index_zmultiples_zsmul (G := Additive G) ?_ i
+  exact (AddSubgroup.eq_top_iff' _).mpr <| (Subgroup.eq_top_iff' ..).mp hg
+
+/-- The subgroups generated by `g ^ i` and `g ^ j` are equal iff
+`i.gcd (orderOf g) = j.gcd (orderOf g)`. Compare `Subgroup.zpowers_eq_zpowers_iff`, which
+characterizes equality of `zpowers x` and `zpowers y` when `x` has infinite order. -/
+@[to_additive /-- The subgroups generated by `i • g` and `j • g` are equal iff
+`i.gcd (addOrderOf g) = j.gcd (addOrderOf g)`. Compare `AddSubgroup.zmultiples_eq_zmultiples_iff`,
+which characterizes equality of `zmultiples x` and `zmultiples y` when `x` has infinite order. -/]
+theorem Subgroup.zpowers_eq_zpowers_iff' [Group G] (g : G) (i j : ℤ) :
+    zpowers (g ^ i) = zpowers (g ^ j) ↔ i.gcd (orderOf g) = j.gcd (orderOf g) := by
+  rw [le_antisymm_iff, zpowers_le_zpowers_iff, zpowers_le_zpowers_iff,
+    Nat.dvd_antisymm_iff, eq_comm]
+
+@[to_additive]
+theorem Subgroup.zpowers_le_zpowers_of_dvd [Group G] (g : G) {m n : ℤ} (h : n ∣ m) :
+    zpowers (g ^ m) ≤ zpowers (g ^ n) :=
+  (zpowers_le_zpowers_iff g m n).mpr (Int.gcd_dvd_gcd_of_dvd_left _ h)
+
+/-- The subgroup generated by `g ^ i` and `g ^ j` is generated by `g ^ gcd i j`. -/
+@[to_additive /-- The subgroup generated by `i • g` and `j • g` is generated by `gcd i j • g`. -/]
+theorem Subgroup.zpowers_zpow_sup [Group G] (g : G) (i j : ℤ) :
+    zpowers (g ^ i) ⊔ zpowers (g ^ j) = zpowers (g ^ (i.gcd j : ℤ)) := by
+  apply le_antisymm
+  · exact sup_le (zpowers_le_zpowers_of_dvd g (gcd_dvd_left i j))
+      (zpowers_le_zpowers_of_dvd g (gcd_dvd_right i j))
+  · grw [Int.gcd_eq_gcd_ab, zpow_add, zpowers_mul_le_sup]
+    exact sup_le_sup (zpowers_le_zpowers_of_dvd g (dvd_mul_right i (i.gcdA j)))
+      (zpowers_le_zpowers_of_dvd g (dvd_mul_right j (i.gcdB j)))
 section addGenerator
 variable [AddGroup G] {g : G} (hg : ∀ x, x ∈ zmultiples g) {n : ℕ} (hn : Nat.card G = n)
 

From 508b9e3b9f8d04d9c2efdb7ec9da0cced5bfc1a4 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Fri, 14 Aug 2026 14:36:29 +0900
Subject: [PATCH 2/3] switch iff

---
 Mathlib/Data/Nat/Basic.lean                    | 4 ++--
 Mathlib/GroupTheory/SpecificGroups/Cyclic.lean | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/Mathlib/Data/Nat/Basic.lean b/Mathlib/Data/Nat/Basic.lean
index 8019798292e80d..968cc4e6062c2a 100644
--- a/Mathlib/Data/Nat/Basic.lean
+++ b/Mathlib/Data/Nat/Basic.lean
@@ -120,8 +120,8 @@ lemma set_induction {S : Set ℕ} (hb : 0 ∈ S) (h_ind : ∀ k : ℕ, k ∈ S 
 /-! ### `mod`, `dvd` -/
 
 /-- Two natural numbers dividing each other are equal. -/
-protected lemma dvd_antisymm_iff : m ∣ n ∧ n ∣ m ↔ m = n :=
-  ⟨fun ⟨h₁, h₂⟩ ↦ Nat.dvd_antisymm h₁ h₂, by simp +contextual⟩
+protected lemma dvd_antisymm_iff : m = n ↔ m ∣ n ∧ n ∣ m :=
+  ⟨by simp +contextual, fun ⟨h₁, h₂⟩ ↦ Nat.dvd_antisymm h₁ h₂⟩
 
 /-- `dvd` is injective in the left argument -/
 lemma dvd_left_injective : Function.Injective ((· ∣ ·) : ℕ → ℕ → Prop) := fun _ _ h =>
diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
index e654aca0a431d2..a18fb59562583f 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -434,7 +434,7 @@ which characterizes equality of `zmultiples x` and `zmultiples y` when `x` has i
 theorem Subgroup.zpowers_eq_zpowers_iff' [Group G] (g : G) (i j : ℤ) :
     zpowers (g ^ i) = zpowers (g ^ j) ↔ i.gcd (orderOf g) = j.gcd (orderOf g) := by
   rw [le_antisymm_iff, zpowers_le_zpowers_iff, zpowers_le_zpowers_iff,
-    Nat.dvd_antisymm_iff, eq_comm]
+    ← Nat.dvd_antisymm_iff, eq_comm]
 
 @[to_additive]
 theorem Subgroup.zpowers_le_zpowers_of_dvd [Group G] (g : G) {m n : ℤ} (h : n ∣ m) :

From cc3b3a97b66008b1f9a0f319f1d7ec6d1e4a9538 Mon Sep 17 00:00:00 2001
From: Xavier Roblot <46200072+xroblot@users.noreply.github.com>
Date: Sat, 15 Aug 2026 08:54:15 +0900
Subject: [PATCH 3/3] review

---
 .../GroupTheory/SpecificGroups/Cyclic.lean    | 28 +++++++++++++++----
 1 file changed, 23 insertions(+), 5 deletions(-)

diff --git a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
index a18fb59562583f..f32eecf957bed0 100644
--- a/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
+++ b/Mathlib/GroupTheory/SpecificGroups/Cyclic.lean
@@ -406,24 +406,42 @@ theorem AddSubgroup.zmultiples_le_zmultiples_iff [AddGroup G] (g : G) (i j : ℤ
     AddSubgroup.map_le_map_iff', zmultiplesHom_ker_eq, Int.zmultiples_sup,
     Int.zmultiples_le_zmultiples_iff, Int.natCast_dvd_natCast]
 
+/-- `zpowers (g ^ i) ≤ zpowers (g ^ j)` iff `j.gcd (orderOf g) ∣ i.gcd (orderOf g)`.
+This characterizes inclusion of cyclic subgroups of a group generated by integer powers of a
+single element. -/
 @[to_additive existing]
 theorem Subgroup.zpowers_le_zpowers_iff [Group G] (g : G) (i j : ℤ) :
     zpowers (g ^ i) ≤ zpowers (g ^ j) ↔ j.gcd (orderOf g) ∣ i.gcd (orderOf g) :=
   AddSubgroup.zmultiples_le_zmultiples_iff (Additive.ofMul g) i j
 
+/-- In any additive group, the index of `zmultiples (i • g)` relative to `zmultiples g` is the
+gcd of `i` and the order of `g`. -/
+theorem AddSubgroup.relIndex_zmultiples_zsmul [AddGroup G] (g : G) (i : ℤ) :
+    (zmultiples (i • g)).relIndex (zmultiples g) = i.gcd (addOrderOf g) := by
+  rw [← zmultiplesHom_apply, ← AddMonoidHom.map_zmultiples, ← range_zmultiplesHom g,
+    AddMonoidHom.range_eq_map, AddSubgroup.relIndex_map_map, top_sup_eq,
+    AddSubgroup.relIndex_top_right, zmultiplesHom_ker_eq, Int.zmultiples_sup,
+    Int.index_zmultiples, Int.natAbs_natCast]
+
+/-- In any group, the index of `zpowers (g ^ i)` relative to `zpowers g` is the gcd of `i` and
+the order of `g`. -/
+@[to_additive existing]
+theorem Subgroup.relIndex_zpowers_zpow [Group G] (g : G) (i : ℤ) :
+    (zpowers (g ^ i)).relIndex (zpowers g) = i.gcd (orderOf g) :=
+  AddSubgroup.relIndex_zmultiples_zsmul (Additive.ofMul g) i
+
 /-- In an additive group generated by `g`, the index of `zmultiples (i • g)` is the gcd of `i`
 and the order of `g`. -/
 theorem AddSubgroup.index_zmultiples_zsmul [AddGroup G] {g : G} (hg : zmultiples g = ⊤) (i : ℤ) :
     (zmultiples (i • g)).index = i.gcd (addOrderOf g) := by
-  rw [← zmultiplesHom_apply, ← AddMonoidHom.map_zmultiples, AddSubgroup.index_map,
-    zmultiplesHom_ker_eq, Int.zmultiples_sup, Int.index_zmultiples, range_zmultiplesHom, hg,
-    AddSubgroup.index_top, mul_one, Int.natAbs_natCast]
+  rw [← AddSubgroup.relIndex_top_right, ← hg, AddSubgroup.relIndex_zmultiples_zsmul]
 
+/-- In a group generated by `g`, the index of `zpowers (g ^ i)` is the gcd of `i` and the order
+of `g`. -/
 @[to_additive existing]
 theorem Subgroup.index_zpowers_zpow [Group G] {g : G} (hg : zpowers g = ⊤) (i : ℤ) :
     (zpowers (g ^ i)).index = i.gcd (orderOf g) := by
-  refine AddSubgroup.index_zmultiples_zsmul (G := Additive G) ?_ i
-  exact (AddSubgroup.eq_top_iff' _).mpr <| (Subgroup.eq_top_iff' ..).mp hg
+  rw [← Subgroup.relIndex_top_right, ← hg, Subgroup.relIndex_zpowers_zpow]
 
 /-- The subgroups generated by `g ^ i` and `g ^ j` are equal iff
 `i.gcd (orderOf g) = j.gcd (orderOf g)`. Compare `Subgroup.zpowers_eq_zpowers_iff`, which