charmatrix_zero — Mathlib

English

The charmatrix of the zero matrix is the zero matrix in polynomial entries except for the diagonal which is X on the diagonal.

Русский

charmatrix нуль-матрицы есть нуль-матрица в полиномах, за исключением диагонали, где элемент X.

LaTeX

$$$\text{charmatrix}(0) = \text{diagonal}(X)$$$

Lean4

@[simp]
theorem charmatrix_zero : charmatrix (0 : Matrix n n R) = Matrix.scalar n (X : R[X]) := by simp [charmatrix]

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