apply

Mathlib.LinearAlgebra.Matrix.Hermitian

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

English

If A is Hermitian, then 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 \Rightarrow \star(A_{j i}) = A_{i j}$ for all i,j$$

Lean4

theorem apply {A : Matrix n n α} (h : A.IsHermitian) (i j : n) : star (A j i) = A i j :=
  congr_fun (congr_fun h _) _

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

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

Разделы

Аффилиация

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