From 005cd10a286624f4afc420d0a6b1d1ad5eda4cf8 Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Thu, 9 May 2024 10:39:40 +0200
Subject: [PATCH] Update partialDeriv.lean

---
 Nevanlinna/partialDeriv.lean | 19 +++++++++++++++++++
 1 file changed, 19 insertions(+)

diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index cd3f922..47d6596 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -93,6 +93,25 @@ lemma partialDeriv_fderiv {f : E → F} (hf : ContDiff 𝕜 2 f) (z a b : E) :
   · simp
 
 
+section restrictScalars
+
+variable (𝕜 : Type*) [NontriviallyNormedField 𝕜]
+variable {𝕜' : Type*} [NontriviallyNormedField 𝕜'] [NormedAlgebra 𝕜 𝕜']
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedSpace 𝕜' E]
+variable [IsScalarTower 𝕜 𝕜' E]
+variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [NormedSpace 𝕜' F]
+variable [IsScalarTower 𝕜 𝕜' F]
+--variable {f : E → F}
+
+theorem partialDeriv_restrictScalars {f : E → F} {v : E} :
+  Differentiable 𝕜' f → partialDeriv 𝕜 v f = partialDeriv 𝕜' v f := by
+  intro hf
+  unfold partialDeriv
+  funext x
+  rw [(hf x).fderiv_restrictScalars 𝕜]
+  simp
+
+
 theorem partialDeriv_comm
   {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
   {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]