diag_submatrix

Mathlib.Data.Matrix.Diagonal

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

English

For any A, the diagonal of the submatrix A|_{e}^{e} equals the function diag(A) composed with e.

Русский

Для любой матрицы A диагональ подматрицы A|_{e}^{e} равна диагонали A, затем по функции e.

LaTeX

$$$\operatorname{diag}(A_{|e}^{|e}) = (\operatorname{diag} A) \circ e$$$

Lean4

theorem diag_submatrix (A : Matrix m m α) (e : l → m) : diag (A.submatrix e e) = A.diag ∘ e :=
  rfl

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

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

Разделы

Аффилиация

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