mathlib3
d9465730 - chore(data/matrix/basic): add `matrix.star_mul_vec` and `matrix.star_vec_mul` (#14248)

Commit
3 years ago
chore(data/matrix/basic): add `matrix.star_mul_vec` and `matrix.star_vec_mul` (#14248) This also generalizes some nearby typeclasses.
Author
Parents
Loading