Theorem: mderiv_eq_zero_iff' (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
z : S
w : T
f : TangentSpace I z →L[ℂ] TangentSpace I w
u : TangentSpace I z
u0 : u ≠ 0
⊢ f u = 0 ↔ f = 0
Tactic:
simp only [mderiv_eq_zero_iff, u0, or_false_iff]
State after:
no goals