mathlib3
e6c26fe3 - chore(analysis/convex/body): downgrade imports (#18185)

Commit
3 years ago
chore(analysis/convex/body): downgrade imports (#18185) Downgrade imports, by generalizing the statements from a normed space to a topological vector space.
Author
Parents
Loading