term_*ᵥ_ — Mathlib

English

The product M *ᵥ v is the vector whose i-th entry is the dot product of row i of M with v.

Русский

Произведение M *ᵥ v даст вектор, чья i-я компонента равна скалярному произведению строки i матрицы M со вектором v.

LaTeX

$$ (M *ᵥ v)(i) = dotProduct (M i _) v$$

Lean4

@[inherit_doc Matrix.mulVec, scoped term_parser 1000]
public meta def «term_*ᵥ_» : Lean.TrailingParserDescr✝ :=
  ParserDescr.trailingNode✝ `Matrix.«term_*ᵥ_» 73 74
    (ParserDescr.binary✝ `andthen (ParserDescr.symbol✝ " *ᵥ ") (ParserDescr.cat✝ `term 73))

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