charmatrix_natCast

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

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

English

The natCast charmatrix equals the diagonal of X minus the natural cast of k.

Русский

NатCast charmatrix равен диагонали X минус натуральная конвертация k.

LaTeX

$$$\text{charmatrix}(\_k) = \text{diag}(X - k)$$$

Lean4

@[simp]
theorem charmatrix_natCast (k : ℕ) : charmatrix (k : Matrix n n R) = diagonal fun _ => X - (k : R[X]) :=
  charmatrix_diagonal _

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

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

Разделы

Аффилиация

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