Mathlib v3 is deprecated. Go to Mathlib v4

Def fin_orthonormal_basis

Modification history

2022-02-19 18:23
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space/pi_L2): Orthonormal basis (#12060) …
Deleted fin_orthonormal_basisView on Github →
2021-11-13 02:46
src/analysis/inner_product_space/projection.lean
feat(analysis/inner_product_space/projection): orthonormal basis subordinate to an `orthogonal_family` (#10208) …
Modified fin_orthonormal_basisView on Github →
2021-09-25 06:48
src/analysis/inner_product_space/basic.lean
refactor(analysis/inner_product_space/*): split big file (#9382) …
Modified fin_orthonormal_basisView on Github →
2021-05-10 07:36
src/analysis/normed_space/inner_product.lean
refactor(*): bundle `is_basis` (#7496) …
Added fin_orthonormal_basisView on Github →