Commit 2025-12-02 19:12 9e76ccd3

feat(Analysis/Distribution): notation for lineDeriv (#32084) This PR defines type classes for notation for the (iterated) line derivative. Its main uses in bundled types of smooth functions and their duals (distributions) and various function spaces (not yet in mathlib). We separate the algebraic properties to avoid the type class search to get hung up on metavariables, in particular it is necessary to have a separate type class for scalar multiplication.