diff --git a/Nevanlinna/laplace.lean b/Nevanlinna/laplace.lean
index b708c98..2694a62 100644
--- a/Nevanlinna/laplace.lean
+++ b/Nevanlinna/laplace.lean
@@ -15,6 +15,7 @@ import Nevanlinna.cauchyRiemann
 import Nevanlinna.partialDeriv
 
 variable {F : Type*} [NormedAddCommGroup F] [NormedSpace ℝ F]
+variable {G : Type*} [NormedAddCommGroup G] [NormedSpace ℝ G]
 
 
 noncomputable def Complex.laplace : (ℂ → F) → (ℂ → F) :=
@@ -43,7 +44,6 @@ theorem laplace_add {f₁ f₂ : ℂ → F} (h₁ : ContDiff ℝ 2 f₁)  (h₂
   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
   intro v
   unfold Complex.laplace
@@ -57,3 +57,18 @@ theorem laplace_smul {f : ℂ → F} (h : ContDiff ℝ 2 f) : ∀ v : ℝ, Compl
   exact h.differentiable one_le_two
   exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
   exact h.differentiable one_le_two
+
+
+theorem laplace_compContLin {f : ℂ → F} {l : F →L[ℝ] G} (h : ContDiff ℝ 2 f) :
+  Complex.laplace (l ∘ f) = l ∘ (Complex.laplace f) := by
+  unfold Complex.laplace
+  rw [partialDeriv_compContLin]
+  rw [partialDeriv_compContLin]
+  rw [partialDeriv_compContLin]
+  rw [partialDeriv_compContLin]
+  simp
+
+  exact (partialDeriv_contDiff ℝ h Complex.I).differentiable le_rfl
+  exact h.differentiable one_le_two
+  exact (partialDeriv_contDiff ℝ h 1).differentiable le_rfl
+  exact h.differentiable one_le_two