Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-04-08 21:12 c3d9cf90

View on Github →

feat(analysis/analytic/basic): change origin of power series (#2327)

feat(analysis/analytic/basic): move basepoint of power series
docstring
Update src/analysis/analytic/basic.lean Co-Authored-By: Scott Morrison scott@tqft.net
Update src/analysis/analytic/basic.lean Co-Authored-By: Scott Morrison scott@tqft.net
Update src/analysis/analytic/basic.lean Co-Authored-By: Scott Morrison scott@tqft.net

Estimated changes

Modified src/analysis/analytic/basic.lean

added def formal_multilinear_series.change_origin

added theorem formal_multilinear_series.change_origin_eval

added theorem formal_multilinear_series.change_origin_has_sum

added theorem formal_multilinear_series.change_origin_radius

added theorem formal_multilinear_series.change_origin_summable_aux1

added theorem formal_multilinear_series.change_origin_summable_aux2

added theorem formal_multilinear_series.change_origin_summable_aux3

added theorem has_fpower_series_on_ball.analytic_at_of_mem

added theorem has_fpower_series_on_ball.change_origin

added theorem is_open_analytic_at

Modified src/topology/instances/ennreal.lean