mathlib3
9acbe588 - feat(normed_space/normed_group_hom): add lemmas (#7468)

Commit

5 years ago

feat(normed_space/normed_group_hom): add lemmas (#7468) From LTE. Written by @PatrickMassot Co-authored-by: Patrick Massot <patrickmassot@free.fr>

Author

riccardobrasca

Parents