Theorem SchwartzMap.integral_mul_deriv_eq_neg_deriv_mul

Modification history

2026-01-19 07:36
Mathlib/Analysis/Distribution/SchwartzSpace/Basic.lean
chore(Analysis/Distribution): split off derivatives from `SchwartzSpace` and create new folder (#34027) …
Modified SchwartzMap.integral_mul_deriv_eq_neg_deriv_mulView on Github →
2025-09-29 20:43
Mathlib/Analysis/Distribution/SchwartzSpace.lean
feat(SchwartzSpace): integration by parts in 1d (#29846)
Added SchwartzMap.integral_mul_deriv_eq_neg_deriv_mulView on Github →