add_mul — Mathlib

English

The product M * N of matrices is the usual matrix product, with (M * N) i k equal to the dot product of the i-th row of M and the k-th column of N.

Русский

Произведение матриц M и N есть обычное перемножение матриц: (M N)_{ik} — скалярное произведение i-й строки M и k-й столбца N.

LaTeX

$$$ (M N)_{ik} = \sum_j M_{ij} N_{jk} $$$

Lean4

protected theorem add_mul [Fintype m] (L M : Matrix l m α) (N : Matrix m n α) : (L + M) * N = L * N + M * N :=
  by
  ext
  apply add_dotProduct

Похожие утверждения