Commit 2024-11-30 21:42 6c4358ea

View on Github →

chore: don't import conformal maps in Behrend's construction (#19638)

Estimated changes

Modified Mathlib/Analysis/Complex/AbsMax.lean

Modified Mathlib/Analysis/Complex/CauchyIntegral.lean

Modified Mathlib/Analysis/Complex/Conformal.lean

added theorem DifferentiableAt.conformalAt

added theorem conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj

Modified Mathlib/Analysis/Complex/RealDeriv.lean

deleted theorem DifferentiableAt.conformalAt

deleted theorem conformalAt_iff_differentiableAt_or_differentiableAt_comp_conj

Modified Mathlib/Analysis/SpecialFunctions/Complex/LogDeriv.lean

Modified Mathlib/Analysis/SpecialFunctions/ExpDeriv.lean

Modified Mathlib/Combinatorics/Additive/AP/Three/Behrend.lean

Modified Mathlib/Geometry/Manifold/Instances/Sphere.lean

Modified Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

Modified Mathlib/NumberTheory/EulerProduct/ExpLog.lean

Modified Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean