mathlib
f6c4e361 - add `normed_field.induced` and `normed_algebra.induced`

Commit

3 years ago

add `normed_field.induced` and `normed_algebra.induced`

Author

j-loreaux

j-loreaux

Parents

Loading