Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-02-22 18:15 d054fcae

View on Github →

feat(/analysis/inner_product_space/pi_L2): inner_matrix_row_row (#12177) The inner product between rows/columns of matrices.

Estimated changes

added theorem inner_matrix_col_col
added theorem inner_matrix_row_row