Theorem coe_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 coe_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 coe_orthonormal_basisView on Github →