mathlib
089f741b - feat(analysis/normed{_space/basic, /field/basic}): add some induced norm structures on subobjects (#17169)

Commit
3 years ago
feat(analysis/normed{_space/basic, /field/basic}): add some induced norm structures on subobjects (#17169)
Author
Parents
Loading