charmatrix_one

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

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

English

For natural number k, charmatrix(k) equals the diagonal matrix with X − k on the diagonal.

Русский

Для целого k ∈ ℕ charmatrix(k) равна диагональной матрице с X − k на диагонали.

LaTeX

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

Lean4

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

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

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

Разделы

Аффилиация

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