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

src/analysis/normed/normed_field.lean

@@ -137,6 +137,13 @@ lemma nnnorm_mul_le (a b : α) : ∥a * b∥₊ ≤ ∥a∥₊ * ∥b∥₊ :=
 by simpa only [←norm_to_nnreal, ←real.to_nnreal_mul (norm_nonneg _)]
   using real.to_nnreal_mono (norm_mul_le _ _)
 
+lemma one_le_norm_one (β) [normed_ring β] [nontrivial β] : 1 ≤ ∥(1 : β)∥ :=
+(le_mul_iff_one_le_left $ norm_pos_iff.mpr (one_ne_zero : (1 : β) ≠ 0)).mp
+  (by simpa only [mul_one] using norm_mul_le (1 : β) 1)
+
+lemma one_le_nnnorm_one (β) [normed_ring β] [nontrivial β] : 1 ≤ ∥(1 : β)∥₊ :=
+one_le_norm_one β
+
 lemma filter.tendsto.zero_mul_is_bounded_under_le {f g : ι → α} {l : filter ι}
   (hf : tendsto f l (𝓝 0)) (hg : is_bounded_under (≤) l (norm ∘ g)) :
   tendsto (λ x, f x * g x) l (𝓝 0) :=