submatrix

Mathlib.LinearAlgebra.Matrix.Hermitian

URI: https://scilib.ai/kg/mathlib#Matrix.IsHermitian.submatrix

← MathLib Explorer

English

If A is Hermitian, then the submatrix A.submatrix f f is Hermitian for any f: m → n.

Русский

Если A эрмитова, то любая подматрица A.submatrix f f тоже эрмитова.

LaTeX

$$(A.submatrix f f)^{\mathsf{H}} = A.submatrix f f$$

Lean4

@[simp]
theorem submatrix {A : Matrix n n α} (h : A.IsHermitian) (f : m → n) : (A.submatrix f f).IsHermitian :=
  (conjTranspose_submatrix _ _ _).trans (h.symm ▸ rfl)

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

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

Разделы

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

Аффилиация

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