Theorem harmonic_is_realOfHolomorphic

Modification history

2026-03-03 09:28
Mathlib/Analysis/Complex/Harmonic/Analytic.lean
chore: rename theorems to comply with mathlib standards (#36026) …
Deleted harmonic_is_realOfHolomorphicView on Github →
2025-09-16 14:41
Mathlib/Analysis/InnerProductSpace/Harmonic/Analytic.lean
feat: mean value theorem for harmonic functions (#29682) …
Added harmonic_is_realOfHolomorphicView on Github →