isolated zeros

Stream: Is there code for X?

[Vincent Beffara]

Is one of these somewhere?

import analysis.analytic.basic
import analysis.complex.basic

open filter

lemma isolated_zeros {f : ℂ → ℂ} (hf : analytic_at ℂ f 0) :
  (∀ᶠ z in nhds 0, f z = 0) ∨ (∀ᶠ z in nhds_within 0 {0}ᶜ, f z ≠ 0) :=
sorry

lemma isolated_zeros' {f : ℂ → ℂ} (hf : analytic_at ℂ f 0) :
  (∃ᶠ z in nhds_within 0 {0}ᶜ, f z = 0) → (∀ᶠ z in nhds 0, f z = 0) :=
sorry

[Vincent Beffara]

... it will be soon :grinning:

https://gist.github.com/vbeffara/0ddc2b65f5553162c448e2596e0d254d

(pending a lot of refactoring)