mvPolynomialX_apply

Mathlib.LinearAlgebra.Matrix.MvPolynomial

URI: https://scilib.ai/kg/mathlib#Matrix.mvPolynomialX_apply

English

The (i, j)-entry of mvPolynomialX is exactly the variable X(i, j).

Русский

Входная (i, j)-я в mvPolynomialX равна переменной X(i, j).

LaTeX

$$$\bigl( \text{mvPolynomialX}_{m,n,R} \bigr)_{ij} = X(i,j).$$$

Lean4

@[simp]
theorem mvPolynomialX_apply [CommSemiring R] (i j) : mvPolynomialX m n R i j = MvPolynomial.X (i, j) :=
  rfl

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru