mathlib

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

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) ```