mathlib

667f2a62 - feat(analysis/normed_space/basic): add `norm_algebra_map_nnreal` (#16709)

feat(analysis/normed_space/basic): add `norm_algebra_map_nnreal` (#16709) This adds `simp` lemmas saying that `∥algebra_map ℝ≥0 𝕜 x∥ = x` and similarly for `∥⬝∥₊` whenever `𝕜` is a normed `ℝ`-algebra and satisfies `norm_one_class`. These are needed separately from `norm_algebra_map'` and `nnnorm_algebra_map'` because `𝕜` cannot be a normed `ℝ≥0`-algebra for the simple reason that `ℝ≥0` is not a normed field.