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

Commits
  • feat(data/fin): append
    sgouezel committed 6 years ago
  • Update fin.lean
    sgouezel committed 6 years ago
  • Update fintype.lean
    sgouezel committed 6 years ago
  • replace but_last with init
    sgouezel committed 6 years ago
  • cons and append commute
    sgouezel committed 6 years ago
  • merge
    sgouezel committed 6 years ago
  • Merge remote-tracking branch 'upstream/master' into append
    sgouezel committed 6 years ago
  • Merge branch 'append' of https://github.com/sgouezel/mathlib into append
    sgouezel committed 6 years ago
  • feat(*/multilinear): better multilinear
    sgouezel committed 6 years ago
  • docstrings
    sgouezel committed 6 years ago
  • snoc
    sgouezel committed 6 years ago
  • fix build
    sgouezel committed 6 years ago
  • comp_snoc and friends
    sgouezel committed 6 years ago
  • merge master
    sgouezel committed 6 years ago
  • refactor(analysis/calculus/times_cont_diff): massive refactor
    sgouezel committed 6 years ago
  • fix docstring
    sgouezel committed 6 years ago
  • merge master
    sgouezel committed 6 years ago
  • move notation
    sgouezel committed 6 years ago
  • Merge remote-tracking branch 'upstream/master' into better_times_cont_diff
    sgouezel committed 6 years ago
  • fix build
    sgouezel committed 6 years ago
  • linter
    sgouezel committed 6 years ago
  • linter again
    sgouezel committed 6 years ago
  • Update src/analysis/calculus/times_cont_diff.lean
    sgouezel committed 6 years ago
  • Update src/analysis/calculus/times_cont_diff.lean
    sgouezel committed 6 years ago
  • Update src/analysis/calculus/times_cont_diff.lean
    sgouezel committed 6 years ago
  • Update src/analysis/calculus/times_cont_diff.lean
    sgouezel committed 6 years ago
  • Update src/analysis/calculus/times_cont_diff.lean
    sgouezel committed 6 years ago
  • curryfication -> currying
    sgouezel committed 6 years ago
  • Merge branch 'master' into better_times_cont_diff
    mergify[bot] committed 6 years ago
Loading