mathlib3

d4c0a118 - refactor(analysis/analytic/basic): refactor `change_origin` (#8282)

refactor(analysis/analytic/basic): refactor `change_origin` (#8282) Now each term of `change_origin` is defined as a sum of a formal power series, so it is clear that each term is an analytic function. Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>