im_star_dotProduct_mulVec_self

Mathlib.LinearAlgebra.Matrix.Hermitian

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

← MathLib Explorer

English

Adjugate of a Hermitian matrix is Hermitian.

Русский

Адъюгат Гермитовой матрицы Гермитова.

LaTeX

$$(\\mathrm{adj}(A))^{\\mathrm{H}} = \\mathrm{adj}(A)$$

Lean4

theorem im_star_dotProduct_mulVec_self [Fintype n] {A : Matrix n n α} (hA : A.IsHermitian) (x : n → α) :
    RCLike.im (star x ⬝ᵥ A *ᵥ x) = 0 := by
  classical exact dotProduct_comm _ (star x) ▸ (isHermitian_iff_isSymmetric.mp hA).im_inner_self_apply _

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

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

Разделы

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

Аффилиация

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