Commit 2025-05-27 22:21 f887d8ee

View on Github →

feat(Analysis/Calculus): derivative and complex conjugation (#25028) Show that if f x is differentiable, so is conj ∘ f ∘ conj, and variations on that theme.

Estimated changes

Modified Mathlib/Analysis/Calculus/Deriv/Basic.lean

added theorem DifferentiableAt.comp_ringHom

added theorem DifferentiableAt.comp_semilinear₁

added theorem HasDerivAt.comp_ringHom

added theorem HasDerivAt.comp_semilinear

Modified Mathlib/Analysis/Calculus/Deriv/Star.lean

added theorem DifferentiableAt.conj_conj

added theorem HasDerivAt.conj_conj

added theorem HasDerivAt.star_conj

Modified Mathlib/Analysis/Calculus/FDeriv/Basic.lean

added theorem DifferentiableAt.comp_semilinear₂

added theorem HasFDerivAt.comp_semilinear

Modified Mathlib/Analysis/Calculus/FDeriv/Star.lean

deleted theorem Differentiable.star

deleted theorem DifferentiableAt.star

added theorem DifferentiableAt.star_star

deleted theorem DifferentiableOn.star

deleted theorem DifferentiableWithinAt.star

added theorem HasFDerivAt.star_star

deleted theorem HasFDerivAtFilter.star

deleted theorem HasStrictFDerivAt.star

Modified Mathlib/Analysis/Normed/Ring/Lemmas.lean

added theorem RingHom.isometry

added theorem RingHomIsometric.inv