ext_iff

Mathlib.LinearAlgebra.Matrix.Hermitian

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

English

A is Hermitian iff for all i,j, star(A_{j i}) = A_{i j}.

Русский

A эрмитова тогда и только тогда, когда для всех i,j выполняется star(A_{j i}) = A_{i j}.

LaTeX

$$$A^{\mathsf{H}} = A \quad\text{iff}\quad \forall i,j,\ star(A_{j i}) = A_{i j}$$$

Lean4

theorem ext_iff {A : Matrix n n α} : A.IsHermitian ↔ ∀ i j, star (A j i) = A i j :=
  ⟨IsHermitian.apply, IsHermitian.ext⟩

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

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

Разделы

Аффилиация

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