Commit 2022-09-30 06:01 667f2a62

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.