Theorems · Theorem · complex analysis

Complex.IsConservativeOn.isExactOn_ball

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E],
  ContinuousOn f (Metric.ball c r) →
    Complex.IsConservativeOn f (Metric.ball c r) → Complex.IsExactOn f (Metric.ball c r)

Morera's theorem for a disk On a disk, a continuous function whose integrals on rectangles vanish, has primitives.

Defined in

Mathlib.Analysis.Complex.HasPrimitives

Cited by

2 results in Mathlib

Foundations

Depth 270 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupNormedSpaceCompleteSpace