Theorem SchwartzMap.integral_mul_laplacian_right_eq_left

Modification history

2026-01-22 02:22
Mathlib/Analysis/Distribution/SchwartzSpace/Deriv.lean
feat(Analysis/Distribution): the Laplacian on Schwartz functions (#33636) …
Added SchwartzMap.integral_mul_laplacian_right_eq_leftView on Github →