isHermitian_submatrix_equiv

Mathlib.LinearAlgebra.Matrix.Hermitian

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

← MathLib Explorer

English

For a bijection e, (A.submatrix e e).IsHermitian ⇔ A.IsHermitian.

Русский

Для биекции e, (A.submatrix e e).IsHermitian ⇔ A.IsHermitian.

LaTeX

$$$ (A.submatrix e e).IsHermitian \iff A.IsHermitian $$$

Lean4

@[simp]
theorem isHermitian_submatrix_equiv {A : Matrix n n α} (e : m ≃ n) : (A.submatrix e e).IsHermitian ↔ A.IsHermitian :=
  ⟨fun h => by simpa using h.submatrix e.symm, fun h => h.submatrix _⟩

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

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

Разделы

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

Аффилиация

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