Theorem InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasis

Modification history

2025-07-04 05:47
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
feat: introduce the Laplace operator (#26302) …
Added InnerProductSpace.laplacianWithin_eq_iteratedFDerivWithin_stdOrthonormalBasisView on Github →