mathlib3
4637e5c8 - refactor(analysis/calculus/times_cont_diff): massive refactor (#2012)

Commit
5 years ago
refactor(analysis/calculus/times_cont_diff): massive refactor (#2012) * feat(data/fin): append * Update fin.lean * Update fintype.lean * replace but_last with init * cons and append commute * feat(*/multilinear): better multilinear * docstrings * snoc * fix build * comp_snoc and friends * refactor(analysis/calculus/times_cont_diff): massive refactor * fix docstring * move notation * fix build * linter * linter again * Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * Update src/analysis/calculus/times_cont_diff.lean Co-Authored-By: Scott Morrison <scott@tqft.net> * curryfication -> currying Co-authored-by: Scott Morrison <scott@tqft.net> Co-authored-by: mergify[bot] <37929162+mergify[bot]@users.noreply.github.com>
Author
Parents
Loading