Update mathlib

2024-11-11 08:46:26 +01:00
parent 6d403874e2
commit f3e951884f
3 changed files with 21 additions and 11 deletions
--- a/Nevanlinna/cauchyRiemann.lean
+++ b/Nevanlinna/cauchyRiemann.lean
@@ -31,7 +31,7 @@ theorem CauchyRiemann₃ : (DifferentiableAt ℂ f z)
  have ContinuousLinearMap.comp_lineDeriv : ∀ w : ℂ, ∀ l : ℂ →L[ℝ] ℝ, lineDeriv ℝ (l ∘ f) z w = l ((fderiv ℝ f z) w) := by
    intro w l
    rw [DifferentiableAt.lineDeriv_eq_fderiv]
-    rw [fderiv.comp]
+    rw [fderiv_comp]
    simp
    fun_prop
    exact h.restrictScalars ℝ