Commit 2021-08-10 18:08 d1b2a548

feat(analysis/normed_space/inner_product): add norm_inner_le_norm (#8601) add this:

lemma norm_inner_le_norm (x y : E) : ∥⟪x, y⟫∥ ≤ ∥x∥ * ∥y∥ :=
(is_R_or_C.norm_eq_abs _).le.trans (abs_inner_le_norm x y)