Theorem InnerProductSpace.HarmonicOnNhd.const_smul

Modification history

2025-07-07 08:02
Mathlib/Analysis/InnerProductSpace/Harmonic/Basic.lean
feat: implement harmonic functions (#26721) …
Added InnerProductSpace.HarmonicOnNhd.const_smulView on Github →