Theorem LineDeriv.iteratedLineDerivOp_zero

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_zero View on Github →

2025-12-02 19:12

Mathlib/Analysis/Distribution/DerivNotation.lean

feat(Analysis/Distribution): notation for `lineDeriv` (#32084) …

Added LineDeriv.iteratedLineDerivOp_zero View on Github →