Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2023-06-02 05:41 a1666563

View on Github →

chore(analysis/convex/specific_functions/deriv): remove unnecessary imports (#19140) I accidentally left some extra imports in this file during the split #19031.

Estimated changes