mathlib

f9571f0f - feat(analysis/normed*): add instances about balls and spheres (#14808)

feat(analysis/normed*): add instances about balls and spheres (#14808) Non-bc change: `has_inv.inv` on the unit circle is now defined using `has_inv.inv` instead of complex conjugation.