Commit 2026-03-03 09:28 e8ea1afc

View on Github →

chore: rename theorems to comply with mathlib standards (#36026) On a suggestion of urkud, rename two theorems, in order to comply with mathlib standards.

Estimated changes

Modified Mathlib/Analysis/Complex/Harmonic/Analytic.lean

added theorem InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_ball_re_eq

added theorem InnerProductSpace.HarmonicOnNhd.exists_analyticOnNhd_univ_re_eq

deleted theorem InnerProductSpace.harmonic_is_realOfHolomorphic_univ

deleted theorem harmonic_is_realOfHolomorphic

Modified Mathlib/Analysis/Complex/Harmonic/Liouville.lean

Modified Mathlib/Analysis/Complex/Harmonic/MeanValue.lean