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