diff --git a/Mathlib.lean b/Mathlib.lean
index 9264cd03c93cf3..8620a9f24a757d 100644
--- a/Mathlib.lean
+++ b/Mathlib.lean
@@ -6830,6 +6830,7 @@ public import Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
 public import Mathlib.RingTheory.MvPolynomial.Tower
 public import Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
 public import Mathlib.RingTheory.MvPowerSeries.Basic
+public import Mathlib.RingTheory.MvPowerSeries.Derivative
 public import Mathlib.RingTheory.MvPowerSeries.Equiv
 public import Mathlib.RingTheory.MvPowerSeries.Evaluation
 public import Mathlib.RingTheory.MvPowerSeries.Expand
diff --git a/Mathlib/RingTheory/MvPowerSeries/Derivative.lean b/Mathlib/RingTheory/MvPowerSeries/Derivative.lean
new file mode 100644
index 00000000000000..2d60ca78c9e679
--- /dev/null
+++ b/Mathlib/RingTheory/MvPowerSeries/Derivative.lean
@@ -0,0 +1,209 @@
+/-
+Copyright (c) 2026 Justus Springer. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Justus Springer
+-/
+module
+
+public import Mathlib.Algebra.MvPolynomial.PDeriv
+public import Mathlib.RingTheory.MvPowerSeries.Inverse
+public import Mathlib.RingTheory.MvPowerSeries.Trunc
+
+/-!
+# Formal partial derivatives of multivariate power series
+
+This file defines `MvPowerSeries.pderiv R i`, the formal partial derivative of a multivariate
+power series with respect to variable `i`, as a
+`Derivation R (MvPowerSeries σ R) (MvPowerSeries σ R)`.
+
+See also `PowerSeries.derivative` for the univariate setting.
+
+## Main definitions
+
+- `MvPowerSeries.pderiv R i`: the formal partial derivative with respect to `i`, as a derivation.
+
+## Main results
+
+- `MvPowerSeries.coeff_pderiv`: coefficient formula
+  `coeff n (pderiv R i f) = coeff (n + single i 1) f * (n i + 1)`.
+- `MvPowerSeries.pderiv_coe`: compatibility with `MvPolynomial.pderiv`.
+- `MvPowerSeries.trunc_pderiv`: truncation commutes with partial differentiation.
+- `MvPowerSeries.pderiv.ext`: a power series is determined by its constant term and its partial
+  derivatives.
+- `MvPowerSeries.pderiv_pow`: power rule.
+- `MvPowerSeries.pderiv_inv`, `MvPowerSeries.pderiv_inv'`: derivative of an inverse.
+
+-/
+
+@[expose] public section
+
+namespace MvPowerSeries
+
+open MvPolynomial Finsupp
+
+variable {σ R : Type*}
+
+section Semiring
+
+variable [Semiring R]
+
+/-- The underlying function of the formal partial derivative with respect to variable `i`.
+This is packaged as a derivation in `MvPowerSeries.pderiv`. -/
+noncomputable def pderivFun (i : σ) (f : MvPowerSeries σ R) : MvPowerSeries σ R :=
+  fun d ↦ coeff (d + single i 1) f * (d i + 1)
+
+theorem coeff_pderivFun {i : σ} (f : MvPowerSeries σ R) (d : σ →₀ ℕ) :
+    coeff d (f.pderivFun i) = coeff (d + single i 1) f * (d i + 1) := by
+  rfl
+
+theorem pderivFun_add {i : σ} (f g : MvPowerSeries σ R) :
+    pderivFun i (f + g) = pderivFun i f + pderivFun i g := by
+  ext
+  rw [coeff_pderivFun, map_add, map_add, coeff_pderivFun, coeff_pderivFun, add_mul]
+
+theorem pderivFun_C {i : σ} (r : R) : pderivFun i (C r) = 0 := by
+  ext n
+  rw [coeff_pderivFun, coeff_add_single_C, zero_mul, (coeff n).map_zero]
+
+theorem pderivFun_one {i : σ} : pderivFun i (1 : MvPowerSeries σ R) = 0 := by
+  rw [← map_one C, pderivFun_C (1 : R)]
+
+end Semiring
+
+section CommSemiring
+
+variable [CommSemiring R]
+
+private theorem pderivFun_coe {i : σ} (f : MvPolynomial σ R) :
+    (f : MvPowerSeries σ R).pderivFun i = f.pderiv i := by
+  ext
+  rw [coeff_pderivFun, coeff_coe, coeff_coe, coeff_pderiv]
+
+private theorem trunc_pderivFun [DecidableEq σ] {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
+    trunc R n (pderivFun i f) = pderiv i (trunc R (n + single i 1) f) := by
+  ext
+  rw [coeff_trunc]
+  split_ifs with h
+  · rw [coeff_pderivFun, coeff_pderiv, coeff_trunc, if_pos (add_lt_add_left h _)]
+  · rw [coeff_pderiv, coeff_trunc, if_neg ((add_lt_add_iff_right _).not.mpr h), zero_mul]
+
+-- A special case of `pderivFun_mul`, used in its proof.
+private theorem pderivFun_coe_mul_coe {i : σ} (f g : MvPolynomial σ R) :
+    pderivFun i (f * g : MvPowerSeries σ R) = f * pderiv i g + g * pderiv i f := by
+  rw [← coe_mul, pderivFun_coe, pderiv_mul, add_comm, mul_comm _ g, ← coe_mul, ← coe_mul,
+    MvPolynomial.coe_add]
+
+private theorem pderivFun_mul {i : σ} (f g : MvPowerSeries σ R) :
+    pderivFun i (f * g) = f • g.pderivFun i + g • f.pderivFun i := by
+  classical
+  ext n
+  have h₁ : n < n + single i 1 := lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩
+  have h₂ : n + single i 1 < n + single i 1 + single i 1 :=
+    lt_def.mpr ⟨self_le_add_right _ _, i, by simp⟩
+  have h₃ : n < n + single i 1 + single i 1 := lt_trans h₁ h₂
+  rw [coeff_pderivFun, map_add, ← coeff_trunc_mul_trunc_eq_coeff_mul _ _ _ h₂, smul_eq_mul,
+    smul_eq_mul, ← coeff_trunc_mul_trunc_eq_coeff_mul₂ _ _ g (f.pderivFun i) h₃ h₁,
+    ← coeff_trunc_mul_trunc_eq_coeff_mul₂ _ _ f (g.pderivFun i) h₃ h₁, trunc_pderivFun,
+    trunc_pderivFun, ← coeff_coe, ← coeff_coe, ← coeff_coe, ← map_add, coe_mul, coe_mul, coe_mul,
+    ← pderivFun_coe_mul_coe, coeff_pderivFun]
+
+private theorem pderivFun_smul {i : σ} (r : R) (f : MvPowerSeries σ R) :
+    pderivFun i (r • f) = r • pderivFun i f := by
+  rw [smul_eq_C_mul, smul_eq_C_mul, pderivFun_mul, pderivFun_C, smul_zero, add_zero, smul_eq_mul]
+
+variable (R) in
+/-- The formal partial derivative of a multivariate formal power series with respect to
+variable `i`, as an `R`-derivation on `MvPowerSeries σ R`. -/
+@[no_expose]
+noncomputable def pderiv (i : σ) : Derivation R (MvPowerSeries σ R) (MvPowerSeries σ R) where
+  toFun := pderivFun i
+  map_add' := pderivFun_add
+  map_smul' := pderivFun_smul
+  map_one_eq_zero' := pderivFun_one
+  leibniz' := pderivFun_mul
+
+@[simp] theorem pderiv_C {i : σ} {r : R} : pderiv R i (C r) = 0 := pderivFun_C r
+
+theorem pderiv_one {i : σ} : pderiv R i 1 = 0 := pderiv_C
+
+theorem coeff_pderiv {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
+    coeff n (pderiv R i f) = coeff (n + single i 1) f * (n i + 1) :=
+  coeff_pderivFun f n
+
+theorem pderiv_coe {i : σ} (f : MvPolynomial σ R) :
+    pderiv R i f = MvPolynomial.pderiv i f := pderivFun_coe f
+
+@[simp]
+theorem pderiv_X_self {i : σ} : pderiv R i (X i) = 1 := by
+  classical
+  ext n
+  simp only [coeff_pderiv, coeff_X, boole_mul, add_eq_right, coeff_one]
+  split_ifs <;> simp_all
+
+@[simp]
+theorem pderiv_X_of_ne {i j : σ} (h : j ≠ i) : pderiv R i (X j) = 0 := by
+  classical
+  ext n
+  simpa only [coeff_pderiv, coeff_X, boole_mul, coeff_zero] using
+    if_neg (ne_iff.mpr ⟨i, by grind [Finsupp.add_apply]⟩)
+
+theorem pderiv_X [DecidableEq σ] (i j : σ) :
+    pderiv R i (X j) = Pi.single (M := fun _ => MvPowerSeries σ R) i 1 j := by
+  by_cases h : i = j
+  · subst h; simp only [pderiv_X_self, Pi.single_eq_same]
+  · grind [pderiv_X_of_ne]
+
+theorem trunc_pderiv [DecidableEq σ] {i : σ} (f : MvPowerSeries σ R) (n : σ →₀ ℕ) :
+    trunc R n (pderiv R i f) = MvPolynomial.pderiv i (trunc R (n + single i 1) f) :=
+  trunc_pderivFun ..
+
+/-- The partial derivative of `g^n` equals `n * g^(n-1) * g'`. -/
+theorem pderiv_pow {i : σ} (g : MvPowerSeries σ R) (n : ℕ) :
+    pderiv R i (g ^ n) = n * g ^ (n - 1) * pderiv R i g := by
+  rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]
+
+end CommSemiring
+
+/-- If `f` and `g` have the same constant term and all partial derivatives, then they are equal.
+
+The `CommRing` assumption is needed because the proof uses `smul_right_inj`, which requires
+cancellation of addition in `R`; `IsAddTorsionFree` alone does not suffice. -/
+theorem pderiv.ext [CommRing R] [IsAddTorsionFree R] {f g : MvPowerSeries σ R}
+    (hD : ∀ i, pderiv R i f = pderiv R i g) (hc : constantCoeff f = constantCoeff g) : f = g := by
+  ext n
+  by_cases h : n = 0
+  · rw [h, coeff_zero_eq_constantCoeff, hc]
+  obtain ⟨i, hi : n i ≠ 0⟩ := ne_iff.mp h
+  have : single i 1 ≤ n := fun j ↦ by
+    by_cases hj : j = i <;> grind [single_eq_same, single_eq_of_ne]
+  have e := congr(coeff (n - single i 1) $(hD i))
+  rwa [coeff_pderiv, coeff_pderiv, tsub_add_cancel_of_le this, coe_tsub, Pi.sub_apply,
+    single_eq_same, Nat.cast_sub (Nat.one_le_iff_ne_zero.mpr hi), Nat.cast_one, sub_add_cancel,
+    mul_comm, ← nsmul_eq_mul, mul_comm, ← nsmul_eq_mul, smul_right_inj hi] at e
+
+@[simp]
+theorem pderiv_inv {i : σ} [CommRing R] (f : (MvPowerSeries σ R)ˣ) :
+    pderiv R i ↑f⁻¹ = -(↑f⁻¹ : MvPowerSeries σ R) ^ 2 * pderiv R i f :=
+  (pderiv R i).leibniz_of_mul_eq_one f.inv_mul
+
+@[simp]
+theorem pderiv_invOf {i : σ} [CommRing R] (f : MvPowerSeries σ R) [Invertible f] :
+    pderiv R i ⅟f = -⅟f ^ 2 * pderiv R i f :=
+  (pderiv R i).leibniz_invOf f
+
+/-
+The following theorem is stated only in the case that `R` is a field. This is because
+there is currently no instance of `Inv (MvPowerSeries σ R)` for more general base rings `R`.
+-/
+
+@[simp]
+theorem pderiv_inv' {i : σ} [Field R] (f : MvPowerSeries σ R) :
+    pderiv R i f⁻¹ = -f⁻¹ ^ 2 * pderiv R i f := by
+  by_cases h : constantCoeff f = 0
+  · suffices f⁻¹ = 0 by
+      rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
+    rwa [MvPowerSeries.inv_eq_zero]
+  apply Derivation.leibniz_of_mul_eq_one
+  exact MvPowerSeries.inv_mul_cancel (h := h)
+
+end MvPowerSeries
diff --git a/Mathlib/RingTheory/PowerSeries/Derivative.lean b/Mathlib/RingTheory/PowerSeries/Derivative.lean
index a3abfe874de99a..c926fb57153ca6 100644
--- a/Mathlib/RingTheory/PowerSeries/Derivative.lean
+++ b/Mathlib/RingTheory/PowerSeries/Derivative.lean
@@ -6,25 +6,31 @@ Authors: Richard M. Hill, Ralf Stephan
 module
 
 public import Mathlib.Algebra.Polynomial.Derivation
-public import Mathlib.RingTheory.Derivation.Basic
-public import Mathlib.RingTheory.PowerSeries.Inverse
+public import Mathlib.RingTheory.MvPowerSeries.Derivative
 public import Mathlib.RingTheory.PowerSeries.Substitution
 
 /-!
-# Definitions
+# Formal derivatives of univariate power series
 
-In this file we define an operation `derivative` (formal differentiation)
-on the ring of formal power series in one variable (over an arbitrary commutative semiring).
+This file defines `PowerSeries.derivative`, the formal derivative of a univariate
+power series, as a `Derivation R R⟦X⟧ R⟦X⟧`.
 
-Under suitable assumptions, we prove that two power series are equal if their derivatives
-are equal and their constant terms are equal. This will give us a simple tool for proving
-power series identities. For example, one can easily prove the power series identity
-$\exp ( \log (1+X)) = 1+X$ by differentiating twice.
+See also `MvPowerSeries.pderiv` for the multivariate setting.
 
-## Main Definition
+## Main definitions
 
-- `PowerSeries.derivative R : Derivation R R⟦X⟧ R⟦X⟧` the formal derivative operation.
-  This is abbreviated `d⁄dX R`.
+- `PowerSeries.derivative`: the formal derivative, as a derivation.
+
+## Main results
+
+- `PowerSeries.coeff_derivative`: coefficient formula
+  `coeff n (d⁄dX R f) = coeff (n + 1) f * (n + 1)`.
+- `PowerSeries.derivative_coe`: compatibility with `Polynomial.derivative`.
+- `PowerSeries.trunc_derivative`: truncation commutes with differentiation.
+- `PowerSeries.derivative.ext`: a power series is determined by its constant term and derivative.
+- `PowerSeries.derivative_pow`: power rule.
+- `PowerSeries.derivative_inv`, `PowerSeries.derivative_inv'`: derivative of an inverse.
+- `PowerSeries.derivative_subst`: chain rule for power series substitution.
 -/
 
 @[expose] public section
@@ -33,168 +39,145 @@ namespace PowerSeries
 
 open Polynomial Derivation Nat
 
-section CommutativeSemiring
-variable {R} [CommSemiring R]
-
-/--
-The formal derivative of a power series in one variable.
-This is defined here as a function, but will be packaged as a
-derivation `derivative` on `R⟦X⟧`.
--/
-noncomputable def derivativeFun (f : R⟦X⟧) : R⟦X⟧ := mk fun n ↦ coeff (n + 1) f * (n + 1)
-
-theorem coeff_derivativeFun (f : R⟦X⟧) (n : ℕ) :
-    coeff n f.derivativeFun = coeff (n + 1) f * (n + 1) := by
-  rw [derivativeFun, coeff_mk]
-
-theorem derivativeFun_coe (f : R[X]) : (f : R⟦X⟧).derivativeFun = derivative f := by
-  ext
-  rw [coeff_derivativeFun, coeff_coe, coeff_coe, coeff_derivative]
-
-theorem derivativeFun_add (f g : R⟦X⟧) :
-    derivativeFun (f + g) = derivativeFun f + derivativeFun g := by
-  ext
-  rw [coeff_derivativeFun, map_add, map_add, coeff_derivativeFun,
-    coeff_derivativeFun, add_mul]
-
-theorem derivativeFun_C (r : R) : derivativeFun (C r) = 0 := by
-  ext n
-  -- Note that `map_zero` didn't get picked up, apparently due to a missing `FunLike.coe`
-  rw [coeff_derivativeFun, coeff_succ_C, zero_mul, (coeff n).map_zero]
-
-theorem trunc_derivativeFun (f : R⟦X⟧) (n : ℕ) :
-    trunc n f.derivativeFun = derivative (trunc (n + 1) f) := by
-  ext d
-  rw [coeff_trunc]
-  split_ifs with h
-  · have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
-    rw [coeff_derivativeFun, coeff_derivative, coeff_trunc, if_pos this]
-  · have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]
-    rw [coeff_derivative, coeff_trunc, if_neg this, zero_mul]
+variable {R : Type*}
 
---A special case of `derivativeFun_mul`, used in its proof.
-private theorem derivativeFun_coe_mul_coe (f g : R[X]) : derivativeFun (f * g : R⟦X⟧) =
-    f * derivative g + g * derivative f := by
-  rw [← coe_mul, derivativeFun_coe, derivative_mul,
-    add_comm, mul_comm _ g, ← coe_mul, ← coe_mul, Polynomial.coe_add]
-
-/-- **Leibniz rule for formal power series**. -/
-theorem derivativeFun_mul (f g : R⟦X⟧) :
-    derivativeFun (f * g) = f • g.derivativeFun + g • f.derivativeFun := by
-  ext n
-  have h₁ : n < n + 1 := lt_succ_self n
-  have h₂ : n < n + 1 + 1 := Nat.lt_add_right _ h₁
-  rw [coeff_derivativeFun, map_add, coeff_mul_eq_coeff_trunc_mul_trunc _ _ (lt_succ_self _),
-    smul_eq_mul, smul_eq_mul, coeff_mul_eq_coeff_trunc_mul_trunc₂ g f.derivativeFun h₂ h₁,
-    coeff_mul_eq_coeff_trunc_mul_trunc₂ f g.derivativeFun h₂ h₁, trunc_derivativeFun,
-    trunc_derivativeFun, ← map_add, ← derivativeFun_coe_mul_coe, coeff_derivativeFun]
-
-theorem derivativeFun_one : derivativeFun (1 : R⟦X⟧) = 0 := by
-  rw [← map_one C, derivativeFun_C (1 : R)]
-
-theorem derivativeFun_smul (r : R) (f : R⟦X⟧) : derivativeFun (r • f) = r • derivativeFun f := by
-  rw [smul_eq_C_mul, smul_eq_C_mul, derivativeFun_mul, derivativeFun_C, smul_zero, add_zero,
-    smul_eq_mul]
+section CommutativeSemiring
 
-variable (R)
+variable [CommSemiring R]
 
+variable (R) in
 /-- The formal derivative of a formal power series -/
-noncomputable def derivative : Derivation R R⟦X⟧ R⟦X⟧ where
-  toFun := derivativeFun
-  map_add' := derivativeFun_add
-  map_smul' := derivativeFun_smul
-  map_one_eq_zero' := derivativeFun_one
-  leibniz' := derivativeFun_mul
+noncomputable def derivative : Derivation R R⟦X⟧ R⟦X⟧ :=
+  MvPowerSeries.pderiv R ()
+
 /-- Abbreviation of `PowerSeries.derivative`, the formal derivative on `R⟦X⟧` -/
 scoped notation "d⁄dX" => derivative
 
-variable {R}
+@[simp] theorem derivative_C {r : R} : d⁄dX R (C r) = 0 := MvPowerSeries.pderiv_C
 
-@[simp] theorem derivative_C (r : R) : d⁄dX R (C r) = 0 := derivativeFun_C r
+theorem derivative_one : d⁄dX R 1 = 0 := MvPowerSeries.pderiv_one
 
 theorem coeff_derivative (f : R⟦X⟧) (n : ℕ) :
-    coeff n (d⁄dX R f) = coeff (n + 1) f * (n + 1) := coeff_derivativeFun f n
+    coeff n (d⁄dX R f) = coeff (n + 1) f * (n + 1) := by
+  simp [coeff, derivative, MvPowerSeries.coeff_pderiv]
 
-theorem derivative_coe (f : R[X]) : d⁄dX R f = Polynomial.derivative f := derivativeFun_coe f
+theorem derivative_coe (f : R[X]) : d⁄dX R f = Polynomial.derivative f := by
+  ext
+  rw [coeff_derivative, coeff_coe, coeff_coe, Polynomial.coeff_derivative]
 
-@[simp] theorem derivative_X : d⁄dX R (X : R⟦X⟧) = 1 := by
-  ext n; simp only [coeff_derivative, coeff_one, coeff_X, boole_mul, add_eq_right]
-  split_ifs <;> simp_all
+@[simp] theorem derivative_X : d⁄dX R (X : R⟦X⟧) = 1 :=
+  MvPowerSeries.pderiv_X_self
 
+-- We can't use `MvPowerSeries.trunc_pderiv` in the following proof,
+-- since `PowerSeries.trunc` is not defined in terms of `MvPowerSeries.trunc`.
 theorem trunc_derivative (f : R⟦X⟧) (n : ℕ) :
-    trunc n (d⁄dX R f) = Polynomial.derivative (trunc (n + 1) f) :=
-  trunc_derivativeFun ..
+    trunc n (d⁄dX R f) = Polynomial.derivative (trunc (n + 1) f) := by
+  ext d
+  rw [coeff_trunc]
+  split_ifs with h
+  · have : d + 1 < n + 1 := succ_lt_succ_iff.2 h
+    rw [coeff_derivative, Polynomial.coeff_derivative, coeff_trunc, if_pos this]
+  · have : ¬d + 1 < n + 1 := by rwa [succ_lt_succ_iff]
+    rw [Polynomial.coeff_derivative, coeff_trunc, if_neg this, zero_mul]
 
 theorem trunc_derivative' (f : R⟦X⟧) (n : ℕ) :
     trunc (n - 1) (d⁄dX R f) = Polynomial.derivative (trunc n f) := by
   cases n <;> simp [trunc_derivative]
 
-end CommutativeSemiring
+/-- The derivative of `g^n` equals `n * g^(n-1) * g'`. -/
+theorem derivative_pow (g : R⟦X⟧) (n : ℕ) :
+    d⁄dX R (g ^ n) = n * g ^ (n - 1) * d⁄dX R g :=
+  MvPowerSeries.pderiv_pow g n
 
-/- In the next lemma, we use `smul_right_inj`, which requires not only `IsAddTorsionFree R`, but
-also cancellation of addition in `R`. For this reason, the next lemma is stated in the case that `R`
-is a `CommRing`. -/
+end CommutativeSemiring
 
 /-- If `f` and `g` have the same constant term and derivative, then they are equal. -/
-theorem derivative.ext {R} [CommRing R] [IsAddTorsionFree R] {f g} (hD : d⁄dX R f = d⁄dX R g)
-    (hc : constantCoeff f = constantCoeff g) : f = g := by
-  ext n
-  cases n with
-  | zero =>
-    rw [coeff_zero_eq_constantCoeff, hc]
-  | succ n =>
-    have equ : coeff n (d⁄dX R f) = coeff n (d⁄dX R g) := by rw [hD]
-    rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
-      mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ
-
-@[simp] theorem derivative_inv {R} [CommRing R] (f : R⟦X⟧ˣ) :
-    d⁄dX R ↑f⁻¹ = -(↑f⁻¹ : R⟦X⟧) ^ 2 * d⁄dX R f := by
-  apply Derivation.leibniz_of_mul_eq_one
-  simp
-
-@[simp] theorem derivative_invOf {R} [CommRing R] (f : R⟦X⟧) [Invertible f] :
-    d⁄dX R ⅟f = -⅟f ^ 2 * d⁄dX R f := by
-  rw [Derivation.leibniz_invOf, smul_eq_mul]
+theorem derivative.ext [CommRing R] [IsAddTorsionFree R] {f g} (hD : d⁄dX R f = d⁄dX R g)
+    (hc : constantCoeff f = constantCoeff g) : f = g :=
+  MvPowerSeries.pderiv.ext (fun _ => hD) hc
+
+@[simp]
+theorem derivative_inv [CommRing R] (f : R⟦X⟧ˣ) :
+    d⁄dX R ↑f⁻¹ = -(↑f⁻¹ : R⟦X⟧) ^ 2 * d⁄dX R f :=
+  MvPowerSeries.pderiv_inv f
+
+@[simp]
+theorem derivative_invOf [CommRing R] (f : R⟦X⟧) [Invertible f] :
+    d⁄dX R ⅟f = -⅟f ^ 2 * d⁄dX R f :=
+  MvPowerSeries.pderiv_invOf f
 
 /-
 The following theorem is stated only in the case that `R` is a field. This is because
 there is currently no instance of `Inv R⟦X⟧` for more general base rings `R`.
 -/
-@[simp] theorem derivative_inv' {R} [Field R] (f : R⟦X⟧) : d⁄dX R f⁻¹ = -f⁻¹ ^ 2 * d⁄dX R f := by
-  by_cases h : constantCoeff f = 0
-  · suffices f⁻¹ = 0 by
-      rw [this, pow_two, zero_mul, neg_zero, zero_mul, map_zero]
-    rwa [MvPowerSeries.inv_eq_zero]
-  apply Derivation.leibniz_of_mul_eq_one
-  exact PowerSeries.inv_mul_cancel (h := h)
 
-/-- The derivative of g^n equals n * g^(n-1) * g'. -/
-theorem derivative_pow (A : Type*) [CommSemiring A] (g : A⟦X⟧) (n : ℕ) :
-    d⁄dX A (g ^ n) = n * g ^ (n - 1) * d⁄dX A g := by
-  rw [Derivation.leibniz_pow, smul_eq_mul, nsmul_eq_mul, mul_assoc]
-
-variable (A : Type*) [CommRing A]
+@[simp] theorem derivative_inv' [Field R] (f : R⟦X⟧) : d⁄dX R f⁻¹ = -f⁻¹ ^ 2 * d⁄dX R f :=
+  MvPowerSeries.pderiv_inv' f
 
 /-- Chain rule for polynomials viewed as power series.  Use `derivative_subst` instead. -/
-private theorem derivative_subst_coe (p : Polynomial A) {g : A⟦X⟧} (hg : HasSubst g) :
-    d⁄dX A ((p : A⟦X⟧).subst g) = (d⁄dX A (p : A⟦X⟧)).subst g * d⁄dX A g := by
-  simp [subst_coe hg, derivative_coe, Derivation.comp_aeval_eq (a := g) (derivative A) p,
+private theorem derivative_subst_coe [CommRing R] (p : Polynomial R) {g : R⟦X⟧} (hg : HasSubst g) :
+    d⁄dX R ((p : R⟦X⟧).subst g) = (d⁄dX R (p : R⟦X⟧)).subst g * d⁄dX R g := by
+  simp [subst_coe hg, derivative_coe, Derivation.comp_aeval_eq (a := g) (derivative R) p,
     smul_eq_mul]
 
-theorem derivative_subst {f g : A⟦X⟧} (hg : HasSubst g) :
-    d⁄dX A (f.subst g) = (d⁄dX A f).subst g * d⁄dX A g := by
+theorem derivative_subst [CommRing R] {f g : R⟦X⟧} (hg : HasSubst g) :
+    d⁄dX R (f.subst g) = (d⁄dX R f).subst g * d⁄dX R g := by
   ext n
   obtain ⟨m, hm⟩ := (hg.eventually_coeff_pow_eq_zero (n + 1)).exists_forall_of_atTop
-  have : coeff (n + 1) (f.subst g) = coeff (n + 1) ((↑(trunc (m + 1) f) : A⟦X⟧).subst g) := by
+  have : coeff (n + 1) (f.subst g) = coeff (n + 1) ((↑(trunc (m + 1) f) : R⟦X⟧).subst g) := by
     rw [coeff_subst' hg, coeff_subst' hg]
     refine finsum_congr fun d ↦ ?_
     obtain hd | hd := lt_or_ge d m
     · rw [coeff_coe_trunc_of_lt (by lia)]
     · simp [coeff_trunc, hd, hm]
-  rw [coeff_derivative, this, ← coeff_derivative, derivative_subst_coe A _ hg, coeff_mul, coeff_mul]
+  rw [coeff_derivative, this, ← coeff_derivative, derivative_subst_coe _ hg, coeff_mul, coeff_mul]
   refine Finset.sum_congr rfl fun ⟨i, j⟩ hij ↦ ?_
   congr 1
   simp only [coeff_subst' hg, coeff_derivative, coeff_coe, coeff_trunc]
   exact finsum_congr fun d ↦ by split_ifs <;> simp (disch := grind [Finset.mem_antidiagonal]) [hm]
 
+section deprecated
+
+variable [CommSemiring R]
+
+/--
+The formal derivative of a power series in one variable.
+This is defined here as a function, but will be packaged as a
+derivation `derivative` on `R⟦X⟧`.
+-/
+@[deprecated derivative (since := "2026-06-26")]
+noncomputable def derivativeFun (f : R⟦X⟧) := (derivative R).toFun f
+
+set_option linter.deprecated false in
+@[deprecated "Use Derivation.map_add" (since := "2026-06-26")]
+theorem derivativeFun_add (f g : R⟦X⟧) :
+    derivativeFun (f + g) = derivativeFun f + derivativeFun g :=
+  (derivative R).map_add f g
+
+set_option linter.deprecated false in
+@[deprecated "Use Derivation.leibniz" (since := "2026-06-26")]
+theorem derivativeFun_mul (f g : R⟦X⟧) :
+    derivativeFun (f * g) = f • g.derivativeFun + g • f.derivativeFun :=
+  (derivative R).leibniz f g
+
+set_option linter.deprecated false in
+@[deprecated "Use Derivation.map_one_eq_zero" (since := "2026-06-26")]
+theorem derivativeFun_one : derivativeFun (1 : R⟦X⟧) = 0 :=
+  (derivative R).map_one_eq_zero
+
+set_option linter.deprecated false in
+@[deprecated "Use Derivation.map_smul" (since := "2026-06-26")]
+theorem derivativeFun_smul (r : R) (f : R⟦X⟧) : derivativeFun (r • f) = r • derivativeFun f :=
+  (derivative R).map_smul r f
+
+@[deprecated (since := "2026-06-26")] alias derivativeFun_C := derivative_C
+
+@[deprecated (since := "2026-06-26")] alias coeff_derivativeFun := coeff_derivative
+
+@[deprecated (since := "2026-06-26")] alias derivativeFun_coe := derivative_coe
+
+@[deprecated (since := "2026-06-26")] alias trunc_derivativeFun := trunc_derivative
+
+end deprecated
+
 end PowerSeries
diff --git a/Mathlib/RingTheory/PowerSeries/Exp.lean b/Mathlib/RingTheory/PowerSeries/Exp.lean
index f884c6491322a4..6eecb8c6e834eb 100644
--- a/Mathlib/RingTheory/PowerSeries/Exp.lean
+++ b/Mathlib/RingTheory/PowerSeries/Exp.lean
@@ -8,6 +8,7 @@ module
 public import Mathlib.Algebra.Algebra.Rat
 public import Mathlib.Data.Nat.Cast.Field
 public import Mathlib.RingTheory.PowerSeries.Derivative
+public import Mathlib.RingTheory.PowerSeries.Inverse
 
 /-!
 # Exponential Power Series