Theorem fderiv_comp'

Modification history

2026-06-04 08:41
Mathlib/Analysis/Calculus/FDeriv/Comp.lean
chore: use `to_fun` to auto-generated eta-expanded versions of `comp` declarations (#34361) …
Deleted fderiv_comp'View on Github →
2024-11-02 14:17
Mathlib/Analysis/Calculus/FDeriv/Comp.lean
chore: expand `fderiv` API (#18512) …
Added fderiv_comp'View on Github →