basic): change origin of power series
#2327

Merged

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

mergify merged 8 commits into master from change_origin

feat(analysis/analytic/basic): move basepoint of power series

969fc1cc

docstring

394b6ad1

Merge remote-tracking branch 'upstream/master' into change_origin

c0bc882f

kim-em commented on 2020-04-08

Update src/analysis/analytic/basic.lean

dedd6132

Update src/analysis/analytic/basic.lean

d4ef664a

Update src/analysis/analytic/basic.lean

83145eff

kim-em added ready-to-merge

kim-em approved these changes on 2020-04-08

Merge branch 'master' into change_origin

c746971d

Merge branch 'master' into change_origin

a886951b

mergify merged c3d9cf90 into master 6 years ago

mergify deleted the change_origin branch 6 years ago

Reviewers

kim-em

Assignees

No one assigned

Labels

ready-to-merge

Milestone

No milestone