mathlib3

a88bc4f7 - feat(analysis/convex): the gauge as a seminorm over is_R_or_C (#14879)

feat(analysis/convex): the gauge as a seminorm over is_R_or_C (#14879) Constructs the gauge for a set on a vector spaces over `is_R_or_C` assuming that the set is convex, balanced and absorbing. The main part of this PR is to show that if a set is balanced then the corresponding gauge has the correct scaling behavior. Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: YaelDillies <yael.dillies@gmail.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com> Co-authored-by: Moritz Doll <doll@uni-bremen.de>