mathlib
d01b55f1 - split(analysis/functional/gauge): Split off `analysis.seminorm` (#12054)

Commit
3 years ago
split(analysis/functional/gauge): Split off `analysis.seminorm` (#12054) Move the Minkowski functional to a new file `analysis.convex.gauge`.
Author
Parents
Loading