Commit 2025-09-15 10:13 df4ef408

View on Github →

feat: equivalence of Complex.IsConservativeOn and DifferentiableOn ℂ for continuous functions on open sets (#29629)

Estimated changes

Modified Mathlib/Analysis/Complex/HasPrimitives.lean

added theorem Complex.IsConservativeOn.mono

added theorem Complex.IsExactOn.differentiableOn

deleted theorem Complex.IsExactOn.isConservativeOn_of_isOpen

added theorem Complex.isConservativeOn_and_continuousOn_iff_isDifferentiableOn