mathlib
c6357eeb - feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis (#15540)

Commit

3 years ago

feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis (#15540) This allows transferring general facts about hilbert bases to orthonormal bases

Author

ADedecker

Parents

f3e89fb4

mathlib c6357eeb - feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis (#15540)

mathlib
c6357eeb - feat(analysis/inner_product_space): in finite dimension, hilbert basis = orthonormal basis (#15540)