Commit 2026-01-08 08:52 6ec3a4ce

View on Github →

chore(Analysis/InnerProductSpace): the Laplacian is k-linear (#33739)

Estimated changes

Modified Mathlib/Analysis/InnerProductSpace/Laplacian.lean

modified theorem InnerProductSpace.laplacianWithin_smul

modified theorem InnerProductSpace.laplacian_smul

modified theorem InnerProductSpace.laplacian_smul_nhds