mathlib3

b5ce4aa2 - feat(analysis/inner_product_space/pi_L2): extend an indexed orthonormal set to an orthonormal basis (#16478)

feat(analysis/inner_product_space/pi_L2): extend an indexed orthonormal set to an orthonormal basis (#16478) Given a finite-dimensional inner product space `E`, a fintype `ι` whose cardinality is the dimension of `E`, and a function `v : ι → E` whose restriction to some set `s` in `ι` is orthonormal, modify `v` to give an orthonormal basis for `E` indexed by `ι` which agrees on `s` with `v`. We already have this lemma for sets (`orthonormal.exists_orthonormal_basis_extension`); this is just some messing round to get the indexed version. Also rename `orthonormal.coe_range` to `orthonormal.to_subtype_range`, matching the naming convention for `linear_independent.to_subtype_range`. Formalized as part of the Sphere Eversion project.