charmatrix_apply_eq

Mathlib.LinearAlgebra.Matrix.Charpoly.Basic

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

← MathLib Explorer

English

The diagonal entry of charmatrix at i,i equals X − M_{ii}.

Русский

Диагональный элемент charmatrix на позиции i,i равен X − M_{ii}.

LaTeX

$$$\big(\text{charmatrix } M\big)_{ii} = X - M_{ii}$$$

Lean4

@[simp]
theorem charmatrix_apply_eq : charmatrix M i i = (X : R[X]) - C (M i i) := by
  simp only [charmatrix, RingHom.mapMatrix_apply, sub_apply, scalar_apply, map_apply, diagonal_apply_eq]

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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