Theorem: mfderiv_ne_zero_iff_deriv_ne_zero (Ray/AnalyticManifold/OneDimension.lean)

State before:
S : Type
inst✝⁵ : TopologicalSpace S
cs : ChartedSpace ℂ S
inst✝⁴ : AnalyticManifold I S
T : Type
inst✝³ : TopologicalSpace T
ct : ChartedSpace ℂ T
inst✝² : AnalyticManifold I T
U : Type
inst✝¹ : TopologicalSpace U
cu : ChartedSpace ℂ U
inst✝ : AnalyticManifold I U
f : ℂ → ℂ
z : ℂ
⊢ mfderiv I I f z ≠ 0 ↔ deriv f z ≠ 0
Tactic:
rw [not_iff_not, mfderiv_eq_zero_iff_deriv_eq_zero]
State after:
no goals