isHermitian_natCast

Mathlib.LinearAlgebra.Matrix.Hermitian

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

English

A diagonal matrix with scalar d on the diagonal is Hermitian.

Русский

Диагональная матрица с одинаковым скаляром d на диагонали Гермитова.

LaTeX

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

Lean4

@[simp]
theorem isHermitian_natCast [DecidableEq n] (d : ℕ) : (d : Matrix n n α).IsHermitian :=
  conjTranspose_natCast _

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

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

Разделы

Аффилиация

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