Commit 2021-11-28 07:21 044f5320

chore(analysis/normed_space/hahn_banach): remove norm' (#10527) For a normed space over ℝ-algebra 𝕜, norm' is currently defined to be algebra_map ℝ 𝕜 ∥x∥. I believe this was introduced before the is_R_or_C construct (including the coercion from ℝ to 𝕜 for [is_R_or_C 𝕜]) joined mathlib. Now that we have these things, it's easy to just say (∥x∥ : 𝕜) instead of norm' 𝕜 ∥x∥, so I don't really think norm' needs to exist any more. (In principle, norm' is more general, since it works for all ℝ-algebras 𝕜 rather than just [is_R_or_C 𝕜]. But I can only really think of applications in theis_R_or_C case, and that's the only way it's used in the library.)