normed_group_quotient): put lemmas inside namespace (#7653)

Commit

4 years ago

fix(analysis/normed_space/normed_group_quotient): put lemmas inside namespace (#7653)

Author

benjamindavidson

Parents