Theorem InnerProductSpace.laplacian_smul_nhds

Modification history

2026-01-08 08:52
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
chore(Analysis/InnerProductSpace): the Laplacian is `k`-linear (#33739)
Modified InnerProductSpace.laplacian_smul_nhdsView on Github →
2025-07-07 08:02
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
feat: implement harmonic functions (#26721) …
Added InnerProductSpace.laplacian_smul_nhdsView on Github →