From aeda1e981d9c11703704609a69c041809d79e98e Mon Sep 17 00:00:00 2001
From: Stefan Kebekus <kebekus@users.noreply.github.com>
Date: Fri, 17 May 2024 09:05:15 +0200
Subject: [PATCH] Update complexHarmonic.lean

---
 Nevanlinna/complexHarmonic.lean | 8 +++++++-
 1 file changed, 7 insertions(+), 1 deletion(-)

diff --git a/Nevanlinna/complexHarmonic.lean b/Nevanlinna/complexHarmonic.lean
index 4977809..bb5ad8f 100644
--- a/Nevanlinna/complexHarmonic.lean
+++ b/Nevanlinna/complexHarmonic.lean
@@ -49,7 +49,7 @@ theorem harmonic_iff_comp_CLE_is_harmonic {f : ℂ → F₁} {l : F₁ ≃L[ℝ]
   · have : l ∘ f = (l : F₁ →L[ℝ] G₁) ∘ f := by rfl
     rw [this]
     exact harmonic_comp_CLM_is_harmonic
-  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by 
+  · have : f = (l.symm : G₁ →L[ℝ] F₁) ∘ l ∘ f := by
       funext z
       unfold Function.comp
       simp
@@ -129,6 +129,12 @@ theorem im_of_holomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ
   exact holomorphic_is_harmonic h
 
 
+theorem antiholomorphic_is_harmonic {f : ℂ → ℂ} (h : Differentiable ℂ f) :
+  Harmonic (Complex.conjCLE ∘ f) := by
+  apply harmonic_iff_comp_CLE_is_harmonic.1
+  exact holomorphic_is_harmonic h
+
+
 theorem log_normSq_of_holomorphic_is_harmonic
   {f : ℂ → ℂ}
   (h₁ : Differentiable ℂ f)