mathlib

4a379da7 - feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth (#15980)

feat(analysis/normed_space/basic): change `homeomorph_unit_ball` to make it obviously smooth (#15980) Formalized as part of the Sphere Eversion project. Co-authored-by: Patrick Massot <patrickmassot@free.fr>