mathlib

baa88307 - feat(analysis/inner_product_space/of_norm): Create an inner product from a norm (#4798)

feat(analysis/inner_product_space/of_norm): Create an inner product from a norm (#4798) A normed space respecting the polarization identity is an inner product space. Co-authored-by: Frédéric Dupuis <dupuisf@iro.umontreal.ca> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Ruben Van de Velde <65514131+Ruben-VandeVelde@users.noreply.github.com> Co-authored-by: Yaël Dillies <yael.dillies@gmail.com>