Theorem DifferentiableWithinAt.star

Modification history

2025-05-27 22:21

Mathlib/Analysis/Calculus/FDeriv/Star.lean

feat(Analysis/Calculus): derivative and complex conjugation (#25028) …

Deleted DifferentiableWithinAt.star View on Github →

2023-05-24 22:02

Mathlib/Analysis/Calculus/FDeriv/Star.lean

feat: port Analysis.Calculus.FDeriv.Star (#4301)

Added DifferentiableWithinAt.star View on Github →