mathlib

a6ca2e8f - feat(analysis/analytic/isolated_zeros): Principle of isolated zeros (#15908)

feat(analysis/analytic/isolated_zeros): Principle of isolated zeros (#15908) Local version: an analytic function is either locally zero, or nonzero in a punctured neighborhood. Co-authored-by: ADedecker <anatolededecker@gmail.com>