Theorem ContinuousMultilinearMap.contDiffAt

Modification history

2024-11-27 09:04
Mathlib/Analysis/Calculus/ContDiff/CPolynomial.lean
chore: avoid importing `ContDiff.Defs` in `FDeriv.Analytic` (#19374) …
Modified ContinuousMultilinearMap.contDiffAtView on Github →
2024-02-06 18:38
Mathlib/Analysis/Calculus/FDeriv/Analytic.lean
feat: define `ContinuousMultilinearMap.linearDeriv` and show it's the `fderiv` (#9846)
Added ContinuousMultilinearMap.contDiffAtView on Github →