Mathlib v3 is deprecated. Go to Mathlib v4

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.

Estimated changes

Modified docs/references.bib

Created src/analysis/inner_product_space/of_norm.lean

added theorem inner_product_space.to_inner_product_spaceable

added theorem inner_product_spaceable.add_left

added theorem inner_product_spaceable.continuous.inner_

added theorem inner_product_spaceable.inner_.conj_symm

added theorem inner_product_spaceable.inner_.norm_sq

added theorem inner_product_spaceable.inner_prop

added theorem inner_product_spaceable.inner_prop_neg_one

added theorem inner_product_spaceable.nat

added theorem nonempty_inner_product_space

Modified src/data/is_R_or_C/basic.lean

added theorem is_R_or_C.norm_I_of_ne_zero