Mathlib v3 is deprecated. Go to Mathlib v4

Theorem orthonormal.inner_left_right_finset

Modification history

2021-07-11 19:28

src/analysis/normed_space/inner_product.lean

feat(analysis/normed_space/inner_product): Bessel's inequality (#8251) …

Added orthonormal.inner_left_right_finset View on Github →