From 6ea989be6b60fb2a8bb4ac357c2ec511c13d9738 Mon Sep 17 00:00:00 2001 From: Stefan Kebekus Date: Thu, 9 May 2024 08:18:55 +0200 Subject: [PATCH] Update partialDeriv.lean --- Nevanlinna/partialDeriv.lean | 10 ++-------- 1 file changed, 2 insertions(+), 8 deletions(-) diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean index ebed05b..cd3f922 100644 --- a/Nevanlinna/partialDeriv.lean +++ b/Nevanlinna/partialDeriv.lean @@ -1,13 +1,7 @@ -import Mathlib.Data.Fin.Tuple.Basic -import Mathlib.Analysis.Complex.Basic -import Mathlib.Analysis.Complex.TaylorSeries -import Mathlib.Analysis.Calculus.LineDeriv.Basic -import Mathlib.Analysis.Calculus.ContDiff.Basic -import Mathlib.Analysis.Calculus.ContDiff.Defs import Mathlib.Analysis.Calculus.FDeriv.Basic -import Mathlib.Analysis.Calculus.FDeriv.Comp -import Mathlib.Analysis.Calculus.FDeriv.Linear import Mathlib.Analysis.Calculus.FDeriv.Symmetric +import Mathlib.Analysis.Calculus.ContDiff.Basic + variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]