Theorem InnerProductSpace.laplacianWithin_smul

Modification history

2026-01-08 08:52
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
chore(Analysis/InnerProductSpace): the Laplacian is `k`-linear (#33739)
Modified InnerProductSpace.laplacianWithin_smulView on Github →
2025-07-04 05:47
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
feat: introduce the Laplace operator (#26302) …
Added InnerProductSpace.laplacianWithin_smulView on Github →