Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2019-03-01 10:20 6363212d

View on Github →

feat(analysis/normed_space/deriv): generalize to spaces over any normed field

Estimated changes