mvPolynomialX — Mathlib

English

A matrix whose (i, j)-entry is the indeterminate X(i, j) of the polynomial ring in two-index variables.

Русский

Матрица, у которой в позиции (i, j) стоит переменная X(i, j) из многочленов в двух индексациях.

LaTeX

$$$\text{mvPolynomialX}_{m,n,R} \in M_{m,n}(MvPolynomial((m\times n),R))$ с единичной вкладкой:$ (i,j) \mapsto X(i,j) $.$$

Lean4

/-- The matrix with variable `X (i,j)` at location `(i,j)`. -/
noncomputable def mvPolynomialX [CommSemiring R] : Matrix m n (MvPolynomial (m × n) R) :=
  of fun i j =>
    MvPolynomial.X
      (i, j)
        -- TODO: set as an equation lemma for `mv_polynomial_X`, see https://github.com/leanprover-community/mathlib4/pull/3024

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