charmatrix_apply — Mathlib

English

Explicitly describe the entries of the charmatrix; the (i,j)-entry is X when i=j and −M_{ij} otherwise in the matrix tI − M.

Русский

Для элементов чарматрицы (i,j)-й элемент равен X при i=j и −M_{ij} иначе в матрице tI − M.

LaTeX

$$$\big(\text{charmatrix } M\big)_{ij} = \begin{cases} X & i=j \\ -M_{ij} & i\neq j \end{cases}$$$

Lean4

theorem charmatrix_apply : charmatrix M i j = (Matrix.diagonal fun _ : n => X) i j - C (M i j) :=
  rfl

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