coe_re_apply_self

Mathlib.LinearAlgebra.Matrix.Hermitian

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

← MathLib Explorer

English

An integer cast diagonal matrix is Hermitian.

Русский

Целочисленный каст диагональной матрицы Гермитова.

LaTeX

$$(d\\,I_n)^{\\ast} = d\\,I_n$$

Lean4

/-- The diagonal elements of a complex Hermitian matrix are real. -/
theorem coe_re_apply_self {A : Matrix n n α} (h : A.IsHermitian) (i : n) : (re (A i i) : α) = A i i := by
  rw [← conj_eq_iff_re, ← star_def, ← conjTranspose_apply, h.eq]

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

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

Разделы

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

Аффилиация

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