α : Type ?u.36688
inst✝² : TopologicalSpace α
E : Type ?u.36694
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
α : Type ?u.36688
inst✝² : TopologicalSpace α
E : Type ?u.36694
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) (f' / f x) x
rw [div_eq_inv_mul]
no goals
α : Type ?u.36688
inst✝² : TopologicalSpace α
E : Type ?u.36694
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → ℂ
f' x : ℂ
h₁ : HasDerivAt f f' x
h₂ : 0 < (f x).re ∨ (f x).im ≠ 0
⊢ HasDerivAt (fun t => log (f t)) ((f x)⁻¹ * f') x
exact (hasStrictDerivAt_log h₂).hasDerivAt.comp x h₁