diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index d26026a..b708c98 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -37,6 +37,11 @@ theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁)  (h₂
   exact (partialDeriv_contDiff ℝ h₂ Complex.I).differentiable le_rfl
   exact h₁.differentiable one_le_two
   exact h₂.differentiable one_le_two
+  exact (partialDeriv_contDiff ℝ h₁ 1).differentiable le_rfl
+  exact (partialDeriv_contDiff ℝ h₂ 1).differentiable le_rfl
+  exact h₁.differentiable one_le_two
+  exact h₂.differentiable one_le_two
+
 
 
 theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Complex.laplace (v • f) = v • (Complex.laplace f) := by
diff --git a/Nevanlinna/partialDeriv.lean b/Nevanlinna/partialDeriv.lean
index 47d6596..6e73723 100644
--- a/Nevanlinna/partialDeriv.lean
+++ b/Nevanlinna/partialDeriv.lean
@@ -6,6 +6,7 @@ import Mathlib.Analysis.Calculus.ContDiff.Basic
 variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
 variable (𝕜)
 
 
@@ -53,7 +54,7 @@ theorem partialDeriv_add₂ {f₁ f₂ : E → F} {v : E} (h₁ : Differentiable
     rw [fderiv_add (h₁ w) (h₂ w)]
 
 
-theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] F} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
+theorem partialDeriv_compContLin {f : E → F} {l : F →L[𝕜] G} {v : E} (h : Differentiable 𝕜 f) : partialDeriv 𝕜 v (l ∘ f) = l ∘ partialDeriv 𝕜 v f := by
   unfold partialDeriv
 
   conv =>