Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-04-20 22:44 b2518bee

View on Github →

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

Estimated changes

added theorem one_le_nnnorm_one
added theorem one_le_norm_one