mathlib3

5ac1dab1 - chore(linear_algebra/matrix/dot_product): weaken typeclasses (#18798)

chore(linear_algebra/matrix/dot_product): weaken typeclasses (#18798) This makes unification slightly harder on Lean, so `: _`s are added. Fixes a stupid error in #18783