mathlib3

9f0d61b4 - fix(analysis/inner_product_space/pi_L2): add missing type cast functions (#18574)

fix(analysis/inner_product_space/pi_L2): add missing type cast functions (#18574) The preferred way to convert between `ι → 𝕜` and `euclidean_space 𝕜 ι` is via `pi_Lp.equiv`, as this preserves the right typing information. We use the local notation `⟪x, y⟫ₑ` to refer the euclidean inner product of `x y : ι → 𝕜`, which inserts the casting within the notation. This adds a new definition `matrix.to_euclidean_lin` as a shorthand to turn a matrix into a `linear_map` over `euclidean_space`. It also generalizes `inner_matrix_row_row` and `inner_matrix_col_col` away from `fin n` to arbitrary index types.