isHermitian_one

Mathlib.LinearAlgebra.Matrix.Hermitian

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

← MathLib Explorer

English

The identity matrix is Hermitian.

Русский

Единичная матрица Гермитова.

LaTeX

$$(1)^{\\ast} = 1$$

Lean4

/-- Note this is more general for matrices than `isSelfAdjoint_one` as it does not
require `Fintype n`, which is necessary for `Monoid (Matrix n n R)`. -/
@[simp]
theorem isHermitian_one [DecidableEq n] : (1 : Matrix n n α).IsHermitian :=
  conjTranspose_one

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

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

Разделы

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

Аффилиация

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