Mathlib v3 is deprecated. Go to Mathlib v4

Theorem matrix.vec_mul_diagonal

Modification history

2021-08-26 13:06

src/data/matrix/basic.lean

feat(*): remove the `fintype` requirement from matrices. (#8810) …

Modified matrix.vec_mul_diagonal View on Github →

2020-04-24 11:13

src/data/matrix/basic.lean

feat(linear_algebra): quadratic forms (#2480) …

Added matrix.vec_mul_diagonal View on Github →