term_ᵥ*_ — Mathlib

English

vecMulVec w v is the matrix with entries w_i * v_j.

Русский

vecMulVec w v — матрица, у которой элементы равны w_i * v_j.

LaTeX

$$vecMulVec w v = matrix with entries w(i) * v(j)$$

Lean4

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

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