diff --git a/Mathlib/Analysis/Analytic/IsolatedZeros.lean b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
index 47acf6695e6992..7fe6aec6df34f0 100644
--- a/Mathlib/Analysis/Analytic/IsolatedZeros.lean
+++ b/Mathlib/Analysis/Analytic/IsolatedZeros.lean
@@ -374,3 +374,21 @@ theorem AnalyticOnNhd.map_codiscreteWithin {U : Set 𝕜} {f : 𝕜 → E}
   fun _ hs ↦ mem_map.1 (preimage_mem_codiscreteWithin hfU h₂f hs)
 
 end PreimgCodiscrete
+
+variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
+
+/-- If `f` is analytic at `s`, then `dslope f z₀` is analytic at `s`. -/
+protected lemma AnalyticAt.dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) :
+    AnalyticAt 𝕜 (dslope f z₀) s := by
+  obtain (rfl | hs) := eq_or_ne s z₀
+  · obtain ⟨p, hp⟩ := hf
+    exact ⟨_, hp.has_fpower_series_dslope_fslope⟩
+  · apply AnalyticAt.congr (f := fun z => (z - z₀)⁻¹ • (f z - f z₀)) (by fun_prop (disch := grind))
+    filter_upwards [isOpen_ne.mem_nhds hs] with z hz using (dslope_of_ne f hz).symm
+
+/-- If `f` is analytic at `s`, then the `n`-th iterated `dslope` of `f` at `z₀`
+is analytic at `s`. -/
+lemma AnalyticAt.iterate_dslope {f : 𝕜 → E} {z₀ s : 𝕜} (hf : AnalyticAt 𝕜 f s) (n : ℕ) :
+    AnalyticAt 𝕜 ((Function.swap dslope z₀)^[n] f) s :=
+  Function.Iterate.rec _ hf (fun _ hf ↦ hf.dslope) n