mathlib

567220c2 - refactor(analysis/inner_product_space/pi_L2): Delete `orthonormal_basis_index` (#16698)

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.