Mathlib v3 is deprecated. Go to Mathlib v4

Def matrix.inner_product_space.of_matrix

Modification history

2023-03-24 21:41
src/linear_algebra/matrix/pos_def.lean
refactor(analysis/inner_product_space/basic): do not extend normed_add_comm_group (#18583) …
Added matrix.inner_product_space.of_matrixView on Github →