diff --git a/Mathlib/Algebra/Group/Subgroup/Basic.lean b/Mathlib/Algebra/Group/Subgroup/Basic.lean
index 2ca5fe50f09d6..f60917ae388d5 100644
--- a/Mathlib/Algebra/Group/Subgroup/Basic.lean
+++ b/Mathlib/Algebra/Group/Subgroup/Basic.lean
@@ -1728,6 +1728,11 @@ attribute [class] AddSubgroup.IsCommutative
 instance IsCommutative.commGroup [h : H.IsCommutative] : CommGroup H :=
   { H.toGroup with mul_comm := h.is_comm.comm }
 
+/-- A subgroup of a commutative group is commutative. -/
+@[to_additive "A subgroup of a commutative group is commutative."]
+instance commGroup_isCommutative {G : Type*} [CommGroup G] (H : Subgroup G) : H.IsCommutative :=
+  ⟨CommMagma.to_isCommutative⟩
+
 @[to_additive]
 instance map_isCommutative (f : G →* G') [H.IsCommutative] : (H.map f).IsCommutative :=
   ⟨⟨by
@@ -1749,6 +1754,11 @@ theorem comap_injective_isCommutative {f : G' →* G} (hf : Injective f) [H.IsCo
 instance subgroupOf_isCommutative [H.IsCommutative] : (H.subgroupOf K).IsCommutative :=
   H.comap_injective_isCommutative Subtype.coe_injective
 
+@[to_additive]
+lemma mul_comm_of_mem_isCommutative [H.IsCommutative] {a b : G} (ha : a ∈ H) (hb : b ∈ H) :
+    a * b = b * a := by
+  simpa only [Submonoid.mk_mul_mk, Subtype.mk.injEq] using mul_comm (⟨a, ha⟩ : H) (⟨b, hb⟩ : H)
+
 end Subgroup
 
 namespace MulEquiv
@@ -1954,6 +1964,11 @@ theorem mem_range {f : G →* N} {y : N} : y ∈ f.range ↔ ∃ x, f x = y :=
 @[to_additive]
 theorem range_eq_map (f : G →* N) : f.range = (⊤ : Subgroup G).map f := by ext; simp
 
+@[to_additive]
+instance range_isCommutative {G : Type*} [CommGroup G] {N : Type*} [Group N] (f : G →* N) :
+    f.range.IsCommutative :=
+  range_eq_map f ▸ Subgroup.map_isCommutative ⊤ f
+
 @[to_additive (attr := simp)]
 theorem restrict_range (f : G →* N) : (f.restrict K).range = K.map f := by
   simp_rw [SetLike.ext_iff, mem_range, mem_map, restrict_apply, SetLike.exists,