times_cont_diff): massive refactor
#2012

Merged

refactor(analysis/calculus/times_cont_diff): massive refactor #2012

mergify merged 29 commits into leanprover-community:master from sgouezel:better_times_cont_diff

feat(data/fin): append

53e9fb49

Update fin.lean

a01d2206

Update fintype.lean

c1fc86c4

replace but_last with init

149da094

cons and append commute

974fe6bb

merge

1a6e5c25

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

7b35c05f

Merge branch 'append' of https://github.com/sgouezel/mathlib into append

1f9017b8

feat(*/multilinear): better multilinear

d55bd941

docstrings

8981720c

snoc

d9cf6518

fix build

5836269f

comp_snoc and friends

104879ad

merge master

9f6655da

refactor(analysis/calculus/times_cont_diff): massive refactor

2d5eba27

sgouezel added blocked-by-other-PR

fix docstring

d1ef4acf

urkud commented on 2020-02-19

kim-em removed blocked-by-other-PR

merge master

410f9f5f

move notation

6f95b663

sgouezel added awaiting-review

Merge remote-tracking branch 'upstream/master' into better_times_cont…

112e1847

fix build

58bd19a6

linter

5e3eca1f

linter again

6d13d352

kim-em commented on 2020-02-24