Theorem SchwartzMap.integral_clm_comp_deriv_right_eq_neg_left

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_clm_comp_deriv_right_eq_neg_leftView on Github →
2025-09-29 20:43
Mathlib/Analysis/Distribution/SchwartzSpace.lean
feat(SchwartzSpace): integration by parts in 1d (#29846)
Added SchwartzMap.integral_clm_comp_deriv_right_eq_neg_leftView on Github →