Theorem InnerProductSpace.bounded_harmonic_on_complex_plane_is_constant

Modification history

2026-03-03 16:04
Mathlib/Analysis/Complex/Harmonic/Liouville.lean
feat: generalize Liouville's theorem for harmonic functions (#36049) …
Modified InnerProductSpace.bounded_harmonic_on_complex_plane_is_constantView on Github →
2026-03-02 19:44
Mathlib/Analysis/Complex/Harmonic/Liouville.lean
feat: Liouville Theorem for harmonic functions (#35640) …
Added InnerProductSpace.bounded_harmonic_on_complex_plane_is_constantView on Github →