# Commit 2023-07-12 21:38 baa88307

View on Github →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.

Mathlib v3 is deprecated. Go to Mathlib v4

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.