English
The product M N of matrices is defined by the rule that the (i,k)-entry of M N is the dot product of the i-th row of M and the k-th column of N; this is the standard matrix multiplication.
Русский
Произведение матриц M N определяется как скалярное произведение i-й строки M и k-й столбца N; это обычное умножение матриц.
LaTeX
$$$ (M N)_{ik} = \sum_j M_{ij} N_{jk} $$$
Lean4
/-- `M * N` is the usual product of matrices `M` and `N`, i.e. we have that
`(M * N) i k` is the dot product of the `i`-th row of `M` by the `k`-th column of `N`.
This is currently only defined when `m` is finite. -/
-- We want to be lower priority than `instHMul`, but without this we can't have operands with
-- implicit dimensions.
@[default_instance 100]
instance [Fintype m] [Mul α] [AddCommMonoid α] : HMul (Matrix l m α) (Matrix m n α) (Matrix l n α) where
hMul M N := fun i k => (fun j => M i j) ⬝ᵥ fun j => N j k
