conjTranspose_eq_diagonal — Mathlib

English

Let M be a square matrix and v a vector. M^H = diag(v) iff M = diag(v^*).

Русский

Пусть M — квадратная матрица, v — вектор. Тогда M^H = diag(v) тогда и только тогда, когда M = diag(v^*).

LaTeX

$$$M^{H} = \operatorname{diag}(v) \iff M = \operatorname{diag}(v^{*})$$$

Lean4

@[simp]
theorem conjTranspose_eq_diagonal [DecidableEq n] [AddMonoid α] [StarAddMonoid α] {M : Matrix n n α} {v : n → α} :
    Mᴴ = diagonal v ↔ M = diagonal (star v) :=
  (Function.Involutive.eq_iff conjTranspose_conjTranspose).trans <| by rw [diagonal_conjTranspose]

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