ring
𝕜 : Type u_1
E : Type u_2
V : Type u_3
r : ℝ
z : ℂ
a b t : ℝ
n✝ n : ℕ
n_pos : 0 < n
f g : ℂ → ℂ
hg : ∀ᶠ (z : ℂ) in 𝓝 z, f z = g z ^ n
g_diff : DifferentiableAt ℂ g z
fz_nonzero : f z ≠ 0
h1 : g z ≠ 0
h2 : ↑n * g z ^ (n - 1) ≠ 0
⊢ deriv g z * (↑n * g z ^ (n - 1)) = ↑n * g z ^ (n - 1) * deriv g z
no goals