conjTranspose_inj

Mathlib.LinearAlgebra.Matrix.ConjTranspose

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

English

For matrices A,B, A^H = B^H if and only if A = B.

Русский

Для матриц A, B, A^H = B^H тогда и только тогда, когда A = B.

LaTeX

$$$A^{H} = B^{H} \iff A = B$$$

Lean4

@[simp]
theorem conjTranspose_inj [InvolutiveStar α] {A B : Matrix m n α} : Aᴴ = Bᴴ ↔ A = B :=
  conjTranspose_injective.eq_iff

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

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

Разделы

Аффилиация

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