mathlib

8ab47c53 - feat(analysis/inner_product_space/basic): `orthonormal` version of `linear_independent.coe_range` (#15577)