pi_L2): change of basis matrix between orthonormal bases is unitary (#16474)

Commit

3 years ago

feat(analysis/inner_product_space/pi_L2): change of basis matrix between orthonormal bases is unitary (#16474) Formalized as part of the Sphere Eversion project.

Author

hrmacbeth

Parents

38963b53

mathlib f058af30 - feat(analysis/inner_product_space/pi_L2): change of basis matrix between orthonormal bases is unitary (#16474)

mathlib
f058af30 - feat(analysis/inner_product_space/pi_L2): change of basis matrix between orthonormal bases is unitary (#16474)