diff --git a/Nevanlinna/test.lean b/Nevanlinna/test.lean index 2739a58..966fde2 100644 --- a/Nevanlinna/test.lean +++ b/Nevanlinna/test.lean @@ -1,6 +1,6 @@ import Mathlib.Analysis.Complex.CauchyIntegral --import Mathlib.Analysis.Complex.Module - +-- test open ComplexConjugate @@ -83,17 +83,17 @@ theorem JensenFormula₂ : rw [← tmp] rw [this] - + have : ∀ z : ℂ, log (Complex.abs z) = 1/2 * Complex.log z + 1/2 * Complex.log (conj z) := by intro z - by_cases argHyp : Complex.arg z = π - + by_cases argHyp : Complex.arg z = π + · rw [Complex.log, argHyp, Complex.log] let ZZ := Complex.arg_conj z rw [argHyp] at ZZ - + simp at ZZ have : conj z = z := by @@ -103,7 +103,7 @@ theorem JensenFormula₂ : let ZZ := Complex.log_conj z nth_rewrite 1 [Complex.log] - + simp let φ := Complex.arg z