mathlib
5b774133 - refactor(analysis/inner_product_space/pi_L2): change `std_orthonormal_basis` to type `orthonormal_basis` (#12253)

Commit
3 years ago
refactor(analysis/inner_product_space/pi_L2): change `std_orthonormal_basis` to type `orthonormal_basis` (#12253) Co-authored-by: Daniel-Packer <62404584+Daniel-Packer@users.noreply.github.com> Co-authored-by: Daniel Packer <62404584+Daniel-Packer@users.noreply.github.com>
Author
Parents
Loading