Theorem Differentiable.clm_apply

Modification history

2025-09-18 12:51
Mathlib/Analysis/Calculus/FDeriv/CompCLM.lean
refactor(Analysis/Calculus/FDeriv): split off material on composing continuous linear maps (#29753) …
Modified Differentiable.clm_applyView on Github →
2023-05-25 11:48
Mathlib/Analysis/Calculus/FDeriv/Mul.lean
feat: port Analysis.Calculus.FDeriv.Mul (#4241)
Added Differentiable.clm_applyView on Github →