add_torsor): nnnorm lemmas (#18997)

Commit

2 years ago

chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997) For every `dist`/`norm` lemma in these files, this adds the corresponding `nndist`/`nnnorm` lemma.

Author

eric-wieser

Parents

729d23f9

mathlib 837f72de - chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997)

mathlib
837f72de - chore(analysis/normed/group/add_torsor): nnnorm lemmas (#18997)