mulᵣ — Mathlib

English

mulᵣ is the dot-product based definition of matrix multiplication with entries from Fin indexing; it coincides with standard matrix multiplication.

Русский

mulᵣ — определение умножения матриц по скалярному произведению с индексами Fin; совпадает с обычным умножением матриц.

LaTeX

$$$A.mulᵣ B = A B$$$

Lean4

/-- `Matrix.mul` with better defeq for `Fin` -/
def mulᵣ [Mul α] [Add α] [Zero α] (A : Matrix (Fin l) (Fin m) α) (B : Matrix (Fin m) (Fin n) α) :
    Matrix (Fin l) (Fin n) α :=
  of <| FinVec.map (fun v₁ => FinVec.map (fun v₂ => dotProductᵣ v₁ v₂) Bᵀ) A

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