mathlib3

4f033b7d - feat(analysis/seminorm): define the Minkowski functional (#9097)

feat(analysis/seminorm): define the Minkowski functional (#9097) This defines the gauge of a set, aka the Minkowski functional, in a vector space over a real normed field. Co-authored-by: <bhavikmehta8@gmail.com>