mathlib
757eaf4f - chore(analysis/calculus/{deriv,mean_value}): use `slope` (#11419)

Commit
4 years ago
chore(analysis/calculus/{deriv,mean_value}): use `slope` (#11419) Co-authored-by: Johan Commelin <johan@commelin.net>
Author
Parents
Loading