mfderiv): add arithmetic lemmas (#17432)

Commit

3 years ago

feat(geometry/manifold/mfderiv): add arithmetic lemmas (#17432) Add `add, mul, sub, neg, const_smul` lemmas for `mfderiv, mdifferentiable_at, mdifferentiable`.

Author

CBirkbeck

Parents

ba169ae3

mathlib3 0616cee2 - feat(geometry/manifold/mfderiv): add arithmetic lemmas (#17432)

mathlib3
0616cee2 - feat(geometry/manifold/mfderiv): add arithmetic lemmas (#17432)