diff --git a/Mathlib.lean b/Mathlib.lean
index 7e56682c7cbb36..43a4a5d42c3e14 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -8179,6 +8179,7 @@ public import Mathlib.Topology.Convenient.OpenClosed
 public import Mathlib.Topology.Covering.AddCircle
 public import Mathlib.Topology.Covering.Basic
 public import Mathlib.Topology.Covering.Deck
+public import Mathlib.Topology.Covering.FundamentalGroupCircle
 public import Mathlib.Topology.Covering.Quotient
 public import Mathlib.Topology.Defs.Basic
 public import Mathlib.Topology.Defs.Filter
diff --git a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean
index 9086a7f8d6c3c1..813967eb8f71ed 100644
--- a/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean
+++ b/Mathlib/Algebra/Group/Subgroup/ZPowers/Lemmas.lean
@@ -50,6 +50,29 @@ namespace AddSubgroup
 theorem range_zmultiplesHom (a : A) : (zmultiplesHom A a).range = zmultiples a :=
   rfl
 
+section IsAddTorsionFree
+
+variable [IsAddTorsionFree A] {a : A}
+
+/-- The subgroup generated by a nonzero element `a` of a torsion-free additive group is isomorphic
+to `ℤ`, sending `n • a` to `n`. -/
+noncomputable def zmultiplesEquivInt (ha : a ≠ 0) : zmultiples a ≃+ ℤ :=
+  ((AddMonoidHom.ofInjective (zmultiplesHom_injective ha)).trans
+    (AddEquiv.addSubgroupCongr (range_zmultiplesHom a))).symm
+
+@[simp]
+theorem coe_zmultiplesEquivInt_symm_apply (ha : a ≠ 0) (n : ℤ) :
+    ((zmultiplesEquivInt ha).symm n : A) = n • a := by
+  simp only [zmultiplesEquivInt, AddEquiv.symm_symm, AddEquiv.trans_apply,
+    AddEquiv.addSubgroupCongr_apply, AddMonoidHom.ofInjective_apply, zmultiplesHom_apply]
+
+@[simp]
+theorem zmultiplesEquivInt_apply_zsmul (ha : a ≠ 0) (n : ℤ) :
+    zmultiplesEquivInt ha ⟨n • a, zsmul_mem_zmultiples a n⟩ = n :=
+  (zmultiplesEquivInt ha).eq_symm_apply.mp (Subtype.ext (by simp))
+
+end IsAddTorsionFree
+
 section Ring
 
 variable {R : Type*} [Ring R] (r : R) (k : ℤ)
diff --git a/Mathlib/Algebra/Group/TypeTags/Basic.lean b/Mathlib/Algebra/Group/TypeTags/Basic.lean
index bc013a65d865c4..60010624de18f8 100644
--- a/Mathlib/Algebra/Group/TypeTags/Basic.lean
+++ b/Mathlib/Algebra/Group/TypeTags/Basic.lean
@@ -483,6 +483,12 @@ instance [Monoid α] [IsMulTorsionFree α] : IsAddTorsionFree (Additive α) wher
 instance [AddMonoid α] [IsAddTorsionFree α] : IsMulTorsionFree (Multiplicative α) where
   pow_left_injective _ := nsmul_right_injective (M := α)
 
+instance [Mul α] [IsMulCommutative α] : IsAddCommutative (Additive α) where
+  is_comm := ⟨fun a b ↦ congrArg Additive.ofMul (mul_comm' a.toMul b.toMul)⟩
+
+instance [Add α] [IsAddCommutative α] : IsMulCommutative (Multiplicative α) where
+  is_comm := ⟨fun a b ↦ congrArg Multiplicative.ofAdd (add_comm' a.toAdd b.toAdd)⟩
+
 /-- If `α` has some multiplicative structure and coerces to a function,
 then `Additive α` should also coerce to the same function.
 
diff --git a/Mathlib/Data/Int/Cast/Lemmas.lean b/Mathlib/Data/Int/Cast/Lemmas.lean
index 2fd2839c02f882..716a3cd2f11b6f 100644
--- a/Mathlib/Data/Int/Cast/Lemmas.lean
+++ b/Mathlib/Data/Int/Cast/Lemmas.lean
@@ -287,6 +287,11 @@ def zpowersHom : α ≃ (Multiplicative ℤ →* α) :=
 
 @[simp] lemma zmultiplesHom_symm_apply (f : ℤ →+ β) : (zmultiplesHom β).symm f = f 1 := rfl
 
+variable {β} in
+lemma zmultiplesHom_injective [IsAddTorsionFree β] {x : β} (hx : x ≠ 0) :
+    Function.Injective (zmultiplesHom β x) :=
+  (injective_iff_map_eq_zero _).2 fun _ hn ↦ (IsAddTorsionFree.zsmul_eq_zero_iff_left hx).1 hn
+
 @[simp] lemma zpowersHom_apply (x : α) (n : Multiplicative ℤ) :
     zpowersHom α x n = x ^ n.toAdd := rfl
 
diff --git a/Mathlib/Topology/Covering/FundamentalGroupCircle.lean b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean
new file mode 100644
index 00000000000000..bef4ed2cbdecaa
--- /dev/null
+++ b/Mathlib/Topology/Covering/FundamentalGroupCircle.lean
@@ -0,0 +1,80 @@
+/-
+Copyright (c) 2026 Ruize Chen. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Ruize Chen
+-/
+module
+
+public import Mathlib.Topology.Covering.AddCircle
+public import Mathlib.Topology.Homotopy.Lifting
+public import Mathlib.Topology.Instances.ZMultiples
+public import Mathlib.Analysis.Convex.Contractible
+
+/-!
+# The fundamental group of the circle
+
+For `0 < p`, the fundamental group of `AddCircle p` at any basepoint is isomorphic to `ℤ`
+(`AddCircle.windingNumberIso`). The winding number `AddCircle.windingNumber` of a loop is
+`(f 1 - f 0) / p` for any continuous lift `f : I → ℝ` of the loop
+(`AddCircle.windingNumber_eq_div`); in particular the loop `t ↦ n • (t * p) + x` has winding
+number `n` (`AddCircle.windingNumber_zsmulLoop`).
+-/
+
+@[expose] public section
+
+open unitInterval
+
+namespace AddCircle
+
+variable (p : ℝ)
+
+/-- The loop in `AddCircle p` based at `x` that winds `n` times, defined as
+`t ↦ n • (t * p) + x`. -/
+def zsmulLoop (x : ℝ) (n : ℤ) : Path (x : AddCircle p) x where
+  toFun t := n • (t * p : ℝ) + x
+  source' := by simp
+  target' := by simp [coe_period]
+  continuous_toFun := by fun_prop
+
+@[simp]
+theorem zsmulLoop_apply (x : ℝ) (n : ℤ) (t : I) :
+    zsmulLoop p x n t = n • (t * p : ℝ) + x :=
+  rfl
+
+variable {p} [hp : Fact (0 < p)]
+
+/-- **The fundamental group of the circle is `ℤ`**: the isomorphism sends the class of a loop to
+its winding number (`windingNumber_eq_div`). It does not depend on the choice of a lift of the
+basepoint (`IsAddQuotientCoveringMap.fundamentalGroupEquiv_eq`). -/
+noncomputable def windingNumberIso (x : AddCircle p) :
+    FundamentalGroup (AddCircle p) x ≃* Multiplicative ℤ :=
+  ((isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x)
+      ⟨(equivIco p 0 x : ℝ), coe_equivIco⟩).trans <|
+    MulOpposite.opMulEquiv.symm.trans (AddSubgroup.zmultiplesEquivInt hp.out.ne').toMultiplicative
+
+/-- The winding number of a loop in `AddCircle p`, defined as its image under `windingNumberIso`. -/
+noncomputable def windingNumber {x : AddCircle p} (γ : FundamentalGroup (AddCircle p) x) : ℤ :=
+  (windingNumberIso x γ).toAdd
+
+/-- The winding number of a loop in `AddCircle p` is `(f 1 - f 0) / p`, for any continuous lift
+`f` of the loop to `ℝ`. -/
+theorem windingNumber_eq_div {x : AddCircle p} (γ : Path x x) (f : C(I, ℝ)) (hf : (↑) ∘ f = γ) :
+    (windingNumber (.mk γ) : ℝ) = (f 1 - f 0) / p := by
+  have h0 : (f 0 : AddCircle p) = x := congr($hf 0).trans γ.source
+  obtain ⟨n, hn⟩ : ∃ n : ℤ, n • p = f 1 - f 0 :=
+    AddSubgroup.mem_zmultiples_iff.mp <| QuotientAddGroup.eq_iff_sub_mem.mp <|
+      congr($hf 1).trans <| γ.target.trans h0.symm
+  have h : (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv (x := x) ⟨f 0, h0⟩ (.mk γ) =
+      .op (.ofAdd ⟨n • p, n, rfl⟩) :=
+    (isAddQuotientCoveringMap_coe p).fundamentalGroupToMulOpposite_apply_mk_eq hf rfl (by simp [hn])
+  simp [windingNumber, windingNumberIso, AddSubgroup.zmultiplesEquivInt_apply_zsmul hp.out.ne' n,
+    (isAddQuotientCoveringMap_coe p).fundamentalGroupEquiv_eq _ ⟨f 0, h0⟩, h,
+    eq_div_iff hp.out.ne', ← zsmul_eq_mul, ← hn]
+
+/-- The loop `t ↦ n • (t * p) + x` has winding number `n`. -/
+theorem windingNumber_zsmulLoop (x : ℝ) (n : ℤ) :
+    windingNumber (x := x) (.mk (zsmulLoop p x n)) = n := by
+  simpa [hp.out.ne'] using windingNumber_eq_div (zsmulLoop p x n)
+    ⟨fun t ↦ n • (t * p) + x, by fun_prop⟩ rfl
+
+end AddCircle
diff --git a/Mathlib/Topology/Homotopy/Lifting.lean b/Mathlib/Topology/Homotopy/Lifting.lean
index f5a47dfa109fb3..67d1e6c41dead7 100644
--- a/Mathlib/Topology/Homotopy/Lifting.lean
+++ b/Mathlib/Topology/Homotopy/Lifting.lean
@@ -392,6 +392,15 @@ def monodromy {x y : X} (γ : Path.Homotopic.Quotient x y) :
       congr($(cov.liftPath_lifts ..) 1).trans γ.target⟩)
     fun _ _ h ↦ Subtype.ext (cov.liftPath_apply_one_eq_of_homotopicRel h ..)
 
+theorem coe_monodromy_mk {x y : X} (γ : Path x y) (e : p ⁻¹' {x}) :
+    (cov.monodromy (.mk γ) e : E) = cov.liftPath γ e (γ.source.trans e.2.symm) 1 :=
+  rfl
+
+lemma monodromy_eq_apply_one {x y : X} {γ : Path x y} {e : p ⁻¹' {x}} {Γ : C(I, E)}
+    (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) : cov.monodromy (.mk γ) e = Γ 1 := by
+  rw [show Γ = cov.liftPath γ e (γ.source.trans e.2.symm) from (eq_liftPath_iff' ..).mpr ⟨hpΓ, Γ_0⟩,
+    coe_monodromy_mk]
+
 /-- Lift a homotopy class of paths to a covering space. -/
 def liftPathQuotient {x y : X} (γ : Path.Homotopic.Quotient x y) (e : p ⁻¹' {x}) :
     Path.Homotopic.Quotient e.1 (cov.monodromy γ e) :=
@@ -647,11 +656,37 @@ theorem fundamentalGroupToMulOpposite_apply_eq_Iff {g : Gᵐᵒᵖ} :
   have := hp.isCancelSMul.right_cancel'
   aesop
 
+variable {e} in
+theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : G} {Γ : C(I, E)}
+    (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) :
+    hp.fundamentalGroupToMulOpposite e (.mk γ) = .op g :=
+  hp.fundamentalGroupToMulOpposite_apply_eq_Iff.mpr <| by
+    simp [hp.isCoveringMap.monodromy_eq_apply_one hpΓ Γ_0, Γ_1]
+
 variable {e} in
 theorem unop_fundamentalGroupToMulOpposite_smul :
     (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e := by
   simp [fundamentalGroupToMulOpposite, fiberEquivGroup_smul_self]
 
+variable {e} in
+/-- Moving the basepoint `e` in the fiber by `g` conjugates `fundamentalGroupToMulOpposite`
+by `g`. -/
+theorem fundamentalGroupToMulOpposite_toPermFiber :
+    hp.fundamentalGroupToMulOpposite (hp.toPermFiber x g e) γ =
+      MulOpposite.op (g * (hp.fundamentalGroupToMulOpposite e γ).unop * g⁻¹) := by
+  rw [fundamentalGroupToMulOpposite_apply_eq_Iff, hp.monodromy_toPermFiber]
+  simp only [MulOpposite.unop_op, toPermFiber_apply_apply_coe,
+    ← hp.unop_fundamentalGroupToMulOpposite_smul, mul_smul, inv_smul_smul]
+
+/-- If `G` is commutative, `fundamentalGroupToMulOpposite` does not depend on the choice of the
+basepoint `e` in the fiber. -/
+theorem fundamentalGroupToMulOpposite_eq [IsMulCommutative G] (e' : p ⁻¹' {x}) :
+    hp.fundamentalGroupToMulOpposite e = hp.fundamentalGroupToMulOpposite e' := by
+  obtain ⟨g, rfl⟩ := hp.exists_toPermFiber_eq e e'
+  ext γ
+  rw [fundamentalGroupToMulOpposite_toPermFiber, mul_comm' g, mul_inv_cancel_right,
+    MulOpposite.op_unop]
+
 variable {e} in
 theorem fundamentalGroupToMulOpposite_eq_one_iff :
     hp.fundamentalGroupToMulOpposite e γ = 1 ↔ hp.isCoveringMap.monodromy γ e = e where
@@ -693,6 +728,12 @@ def fundamentalGroupEquiv [SimplyConnectedSpace E] :
     ⟨hp.fundamentalGroupToMulOpposite_injective e,
      hp.fundamentalGroupToMulOpposite_surjective e⟩
 
+/-- If `G` is commutative, `fundamentalGroupEquiv` does not depend on the choice of the
+basepoint `e` in the fiber. -/
+theorem fundamentalGroupEquiv_eq [SimplyConnectedSpace E] [IsMulCommutative G] (e' : p ⁻¹' {x}) :
+    hp.fundamentalGroupEquiv e = hp.fundamentalGroupEquiv e' :=
+  MulEquiv.ext fun γ ↦ congr($(hp.fundamentalGroupToMulOpposite_eq e e') γ)
+
 end IsQuotientCoveringMap
 
 namespace IsAddQuotientCoveringMap
@@ -745,11 +786,33 @@ theorem fundamentalGroupToMulOpposite_apply_eq_Iff {g : (Multiplicative G)ᵐᵒ
     hp.fundamentalGroupToMulOpposite e γ = g ↔ g.unop • e.1 = hp.isCoveringMap.monodromy γ e :=
   hp.toMultiplicative.fundamentalGroupToMulOpposite_apply_eq_Iff
 
+variable {e} in
+theorem fundamentalGroupToMulOpposite_apply_mk_eq {γ : Path x x} {g : Multiplicative G}
+    {Γ : C(I, E)} (hpΓ : p ∘ Γ = γ) (Γ_0 : Γ 0 = e) (Γ_1 : Γ 1 = g • e) :
+    hp.fundamentalGroupToMulOpposite e (.mk γ) = .op g :=
+  hp.fundamentalGroupToMulOpposite_apply_eq_Iff.mpr <| by
+    rw [hp.isCoveringMap.monodromy_eq_apply_one hpΓ Γ_0, Γ_1]; rfl
+
 variable {e} in
 theorem unop_fundamentalGroupToMulOpposite_smul :
     (hp.fundamentalGroupToMulOpposite e γ).unop • e.1 = hp.isCoveringMap.monodromy γ e :=
   hp.toMultiplicative.unop_fundamentalGroupToMulOpposite_smul
 
+variable {e} in
+/-- Moving the basepoint `e` in the fiber by `g` conjugates `fundamentalGroupToMulOpposite`
+by `g`. -/
+theorem fundamentalGroupToMulOpposite_toPermFiber :
+    hp.fundamentalGroupToMulOpposite (hp.toMultiplicative.toPermFiber x g e) γ =
+      MulOpposite.op (Multiplicative.ofAdd g * (hp.fundamentalGroupToMulOpposite e γ).unop *
+        (Multiplicative.ofAdd g)⁻¹) :=
+  hp.toMultiplicative.fundamentalGroupToMulOpposite_toPermFiber
+
+/-- If `G` is commutative, `fundamentalGroupToMulOpposite` does not depend on the choice of the
+basepoint `e` in the fiber. -/
+theorem fundamentalGroupToMulOpposite_eq [IsAddCommutative G] (e' : p ⁻¹' {x}) :
+    hp.fundamentalGroupToMulOpposite e = hp.fundamentalGroupToMulOpposite e' :=
+  hp.toMultiplicative.fundamentalGroupToMulOpposite_eq e e'
+
 variable {e} in
 theorem fundamentalGroupToMulOpposite_eq_one_iff :
     hp.fundamentalGroupToMulOpposite e γ = 1 ↔ hp.isCoveringMap.monodromy γ e = e :=
@@ -773,4 +836,10 @@ def fundamentalGroupEquiv [SimplyConnectedSpace E] :
     FundamentalGroup X x ≃* (Multiplicative G)ᵐᵒᵖ :=
   hp.toMultiplicative.fundamentalGroupEquiv e
 
+/-- If `G` is commutative, `fundamentalGroupEquiv` does not depend on the choice of the
+basepoint `e` in the fiber. -/
+theorem fundamentalGroupEquiv_eq [SimplyConnectedSpace E] [IsAddCommutative G] (e' : p ⁻¹' {x}) :
+    hp.fundamentalGroupEquiv e = hp.fundamentalGroupEquiv e' :=
+  hp.toMultiplicative.fundamentalGroupEquiv_eq e e'
+
 end IsAddQuotientCoveringMap