Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-12-11 11:06 97417665

View on Github →

feat(analysis/normed_space): normed space is homeomorphic to the unit ball (#10690)

Estimated changes