normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)

Commit

3 years ago

feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556) Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Author

j-loreaux

Parents

81c8f310

mathlib b2518bee - feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)

mathlib
b2518bee - feat(analysis/normed/normed_field): add `one_le_(nn)norm_one` for nontrivial normed rings (#13556)