feat(analysis/normed_space/basic): generalize submodule.normed_space (#…

…6766)

This means that a ℂ-submodule of an ℝ-normed space is still an ℝ-normed space.

There's too much randomness in the profiling for me to tell if this speeds up or slows down `exists_extension_norm_eq`; but it does at least save a line there.

src/analysis/normed_space/basic.lean

@@ -1165,8 +1165,10 @@ instance pi.normed_space {E : ι → Type*} [fintype ι] [∀i, normed_group (E
     by simp only [(nnreal.coe_mul _ _).symm, nnreal.mul_finset_sup, nnnorm_smul] }
 
 /-- A subspace of a normed space is also a normed space, with the restriction of the norm. -/
-instance submodule.normed_space {𝕜 : Type*} [normed_field 𝕜]
-  {E : Type*} [normed_group E] [normed_space 𝕜 E] (s : submodule 𝕜 E) : normed_space 𝕜 s :=
+instance submodule.normed_space {𝕜 R : Type*} [has_scalar 𝕜 R] [normed_field 𝕜] [ring R]
+  {E : Type*} [normed_group E] [normed_space 𝕜 E] [semimodule R E]
+  [is_scalar_tower 𝕜 R E] (s : submodule R E) :
+  normed_space 𝕜 s :=
 { norm_smul_le := λc x, le_of_eq $ norm_smul c (x : E) }
 
 end normed_space

src/analysis/normed_space/hahn_banach.lean

@@ -82,7 +82,6 @@ begin
   letI : module ℝ F := restrict_scalars.semimodule ℝ 𝕜 F,
   letI : is_scalar_tower ℝ 𝕜 F := restrict_scalars.is_scalar_tower _ _ _,
   letI : normed_space ℝ F := normed_space.restrict_scalars _ 𝕜 _,
-  letI : normed_space ℝ p := (by apply_instance : normed_space ℝ (submodule.restrict_scalars ℝ p)),
   -- Let `fr: p →L[ℝ] ℝ` be the real part of `f`.
   let fr := re_clm.comp (f.restrict_scalars ℝ),
   have fr_apply : ∀ x, fr x = re (f x) := λ x, rfl,