conjTranspose_one

Mathlib.LinearAlgebra.Matrix.ConjTranspose

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

English

The conjugate transpose of the identity matrix is the identity: I^H = I.

Русский

Сопряженно-транспонированная единичная матрица сохраняет единичность: I^H = I.

LaTeX

$$$I^{H} = I$$$

Lean4

@[simp]
theorem conjTranspose_one [DecidableEq n] [NonAssocSemiring α] [StarRing α] : (1 : Matrix n n α)ᴴ = 1 := by
  simp [conjTranspose]

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

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

Разделы

Аффилиация

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