Theorem ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhds

Modification history

2025-07-07 08:02
Mathlib/Analysis/InnerProductSpace/Laplacian.lean
feat: implement harmonic functions (#26721) …
Added ContDiffWithinAt.laplacianWithin_CLM_comp_left_nhdsView on Github →