Commit 2022-10-01 18:32 567220c2
View on Github →refactor(analysis/inner_product_space/pi_L2): Delete orthonormal_basis_index (#16698)
std_orthonormal_basis was indexed by orthonormal_basis_index while it can simply be indexed by fin (finrank 𝕜 E). As a result, fin_std_orthonormal_basis becomes a trivial reindexation of std_orthonormal_basis so we delete it.