mathlib
abc0cbee - chore(analysis/normed_space/basic): reorder the definitions

Commit
3 years ago
chore(analysis/normed_space/basic): reorder the definitions This also update the docstrings to make `normed_space.restrict_scalars` even scarier.
Author
Committer
Parents
Loading