Commit 2023-06-14 02:22 7a82f169

View on Github →

feat: port Analysis.Analytic.Uniqueness (#5029)

Estimated changes

Modified Mathlib.lean

Created Mathlib/Analysis/Analytic/Uniqueness.lean

added theorem AnalyticOn.eqOn_of_preconnected_of_eventuallyEq

added theorem AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero

added theorem AnalyticOn.eqOn_zero_of_preconnected_of_eventuallyEq_zero_aux

added theorem AnalyticOn.eq_of_eventuallyEq