Commit 2026-01-27 21:38 34ea2950

View on Github →

feat(Analysis/Distribution/DerivNotation): simp lemmas for 0 and neg (#34287)

Estimated changes

Modified Mathlib/Analysis/Distribution/DerivNotation.lean

modified theorem LineDeriv.iteratedLineDerivOp_add

added theorem LineDeriv.iteratedLineDerivOp_fin_zero

added theorem LineDeriv.iteratedLineDerivOp_neg

added theorem LineDeriv.iteratedLineDerivOp_sum

modified theorem LineDeriv.iteratedLineDerivOp_zero

added theorem LineDeriv.lineDerivOp_left_neg

added theorem LineDeriv.lineDerivOp_left_sum

added theorem LineDeriv.lineDerivOp_left_zero

added theorem LineDeriv.lineDerivOp_neg

added theorem LineDeriv.lineDerivOp_sum

added theorem LineDeriv.lineDerivOp_zero

Modified Mathlib/Analysis/Distribution/SchwartzSpace/Fourier.lean