Theorem ContinuousLinearEquiv.iteratedFDeriv_comp_left

Modification history

2025-07-04 05:47
Mathlib/Analysis/Calculus/ContDiff/Basic.lean
feat: introduce the Laplace operator (#26302) …
Added ContinuousLinearEquiv.iteratedFDeriv_comp_leftView on Github →