conjTranspose_eq_one

Mathlib.LinearAlgebra.Matrix.ConjTranspose

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

← MathLib Explorer

English

If A^H = B^H then A = B.

Русский

Если A^H = B^H, то A = B.

LaTeX

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

Lean4

@[simp]
theorem conjTranspose_eq_one [DecidableEq n] [NonAssocSemiring α] [StarRing α] {M : Matrix n n α} : Mᴴ = 1 ↔ M = 1 :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <| by rw [conjTranspose_one]

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

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

Разделы

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

Аффилиация

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