isHermitian_intCast

Mathlib.LinearAlgebra.Matrix.Hermitian

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

English

An integer cast diagonal matrix is Hermitian.

Русский

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

LaTeX

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

Lean4

@[simp]
theorem isHermitian_intCast [DecidableEq n] (d : ℤ) : (d : Matrix n n α).IsHermitian :=
  conjTranspose_intCast _

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

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

Разделы

Аффилиация

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