mathlib
f3eaa34d - generalize `(semi)normed_add_comm_group.induced` to hom class

Commit

3 years ago

generalize `(semi)normed_add_comm_group.induced` to hom class

Author

j-loreaux

j-loreaux

Parents

Loading