mathlib3
73e41c24 - feat(analysis/inner_product_space/[pi_L2, l2_space]): compute inner product in a given [orthonormal, hilbert] basis (#15514)

Commit
3 years ago
feat(analysis/inner_product_space/[pi_L2, l2_space]): compute inner product in a given [orthonormal, hilbert] basis (#15514)
Author
Parents
Loading