Commit 2023-06-14 11:00 253d2d89

View on Github →

feat: port Analysis.Analytic.IsolatedZeros (#5038)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Analytic/IsolatedZeros.lean

added theorem AnalyticAt.eventually_eq_or_eventually_ne

added theorem AnalyticAt.eventually_eq_zero_or_eventually_ne_zero

added theorem AnalyticAt.frequently_eq_iff_eventually_eq

added theorem AnalyticAt.frequently_zero_iff_eventually_zero

added theorem AnalyticOn.eqOn_of_preconnected_of_frequently_eq

added theorem AnalyticOn.eqOn_of_preconnected_of_mem_closure

added theorem AnalyticOn.eqOn_zero_of_preconnected_of_frequently_eq_zero

added theorem AnalyticOn.eqOn_zero_of_preconnected_of_mem_closure

added theorem AnalyticOn.eq_of_frequently_eq

added theorem HasFPowerSeriesAt.eq_pow_order_mul_iterate_dslope

added theorem HasFPowerSeriesAt.has_fpower_series_dslope_fslope

added theorem HasFPowerSeriesAt.has_fpower_series_iterate_dslope_fslope

added theorem HasFPowerSeriesAt.iterate_dslope_fslope_ne_zero

added theorem HasFPowerSeriesAt.locally_ne_zero

added theorem HasFPowerSeriesAt.locally_zero_iff

added theorem HasSum.exists_hasSum_smul_of_apply_eq_zero

added theorem HasSum.hasSum_at_zero