Theorem AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_top

Modification history

2025-06-10 11:05
Mathlib/Analysis/Analytic/Order.lean
feat: improve API for isolated zeros of analytic functions (#25643) …
Added AnalyticOnNhd.codiscreteWithin_setOf_analyticOrderAt_eq_zero_or_topView on Github →