Commit 2023-03-17 14:58 9f0d61b4

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.