Commit 2025-06-10 11:05 b19461d8
View on Github →feat: improve API for isolated zeros of analytic functions (#25643)
Use the new definition analyticOrderAt to provide a version of AnalyticOnNhd.codiscrete_setOf_analyticOrderAt_eq_zero_or_top that is easier to use, since it avoids hassle with subtypes and subsets. Provide easy-to-use special cases about the discreteness of the zero locus of analytic functions.