Theorem DifferentiableOn.star

Modification history

2025-05-27 22:21

Mathlib/Analysis/Calculus/FDeriv/Star.lean

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

Deleted DifferentiableOn.star View on Github →

2023-05-24 22:02

Mathlib/Analysis/Calculus/FDeriv/Star.lean

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

Added DifferentiableOn.star View on Github →