mul_apply' — Mathlib

English

The entry (i,k) of M * N equals the dot product of row i of M with column k of N: (M * N)_{ik} = dotProduct( j ↦ M_{ij} )( j ↦ N_{jk} ).

Русский

Элемент (i,k) произведения M и N равен скалярному произведению строки i матрицы M и столбца k матрицы N.

LaTeX

$$$(M * N)_{ik} = \operatorname{dotProduct}(\lambda j, M_{ij})(\lambda j, N_{jk})$$$

Lean4

theorem mul_apply' {l : Type*} [Fintype m] [Mul A] [AddCommMonoid A] {M : CStarMatrix l m A} {N : CStarMatrix m n A}
    {i k} : (M * N) i k = (fun j => M i j) ⬝ᵥ fun j => N j k :=
  rfl

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