mathlib3
3bce8d80 - chore(analysis/calculus/deriv): split file (#19113)

Commit
2 years ago
chore(analysis/calculus/deriv): split file (#19113) * Split `analysis.calculus.deriv` into smaller files. * Add copyright headers and (stubs of) module docstrings. * Change proofs of derivatives of `pow` and `polynomial` so that `analysis.calculus.deriv.pow` does not depend on polynomials. Co-authored-by: Parcly Taxel <reddeloostw@gmail.com> Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Author
Parents
Loading