Mathlib v3 is deprecated. Go to Mathlib v4

Theorem analytic_on.eq_on_zero_of_preconnected_of_eventually_eq_zero

Modification history

2022-10-11 03:45

src/analysis/analytic/uniqueness.lean

feat(analysis/analytic/uniqueness): two analytic functions that coincide locally coincide globally (#16723) …

Added analytic_on.eq_on_zero_of_preconnected_of_eventually_eq_zero View on Github →