Theorem LineDeriv.iteratedLineDerivOp_add

Modification history

2026-01-27 21:38
Mathlib/Analysis/Distribution/DerivNotation.lean
feat(Analysis/Distribution/DerivNotation): `simp` lemmas for `0` and `neg` (#34287)
Modified LineDeriv.iteratedLineDerivOp_addView on Github →
2026-01-22 02:22
Mathlib/Analysis/Distribution/DerivNotation.lean
feat(Analysis/Distribution): the Laplacian on Schwartz functions (#33636) …
Modified LineDeriv.iteratedLineDerivOp_addView on Github →
2025-12-02 19:12
Mathlib/Analysis/Distribution/DerivNotation.lean
feat(Analysis/Distribution): notation for `lineDeriv` (#32084) …
Added LineDeriv.iteratedLineDerivOp_addView on Github →