feat(analysis/normed_space/inner_product): Define the inner product b…

…ased on `is_R_or_C` (#4057)

src/analysis/normed_space/basic.lean

@@ -812,6 +812,9 @@ begin
     rwa [ne.def, norm_eq_zero] }
 end
 
+@[simp] lemma abs_norm_eq_norm (z : β) : abs ∥z∥ = ∥z∥ :=
+  (abs_eq (norm_nonneg z)).mpr (or.inl rfl)
+
 lemma dist_smul [normed_space α β] (s : α) (x y : β) : dist (s • x) (s • y) = ∥s∥ * dist x y :=
 by simp only [dist_eq_norm, (norm_smul _ _).symm, smul_sub]
 

src/analysis/normed_space/hahn_banach.lean

@@ -93,11 +93,11 @@ variables {F : Type*} [normed_group F] [normed_space ℂ F]
 -- Inlining the following two definitions causes a type mismatch between
 -- subspace ℝ (semimodule.restrict_scalars ℝ ℂ F) and subspace ℂ F.
 /-- Restrict a `ℂ`-subspace to an `ℝ`-subspace. -/
-noncomputable def restrict_scalars (p : subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ ℂ F
+noncomputable def restrict_scalars (p : subspace ℂ F) : subspace ℝ F := p.restrict_scalars ℝ
 
 private lemma apply_real (p : subspace ℂ F) (f' : p →L[ℝ] ℝ) :
   ∃ g : F →L[ℝ] ℝ, (∀ x : restrict_scalars p, g x = f' x) ∧ ∥g∥ = ∥f'∥ :=
-  exists_extension_norm_eq (p.restrict_scalars ℝ ℂ F) f'
+  exists_extension_norm_eq (p.restrict_scalars ℝ) f'
 
 open complex