Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2022-05-22 23:41 d9465730

View on Github →

chore(data/matrix/basic): add matrix.star_mul_vec and matrix.star_vec_mul (#14248) This also generalizes some nearby typeclasses.

Estimated changes

Modified src/data/matrix/basic.lean

added theorem matrix.mul_vec_conj_transpose

modified theorem matrix.mul_vec_mul_vec

added theorem matrix.star_mul_vec

added theorem matrix.star_vec_mul

added theorem matrix.vec_mul_conj_transpose

modified theorem matrix.vec_mul_vec_mul