diagonal_conjTranspose — Mathlib

English

Conjugate transpose passes through diagonals: diag Aᴴ = diag(star A).

Русский

Сопряженное транспонирование проходит через диагонали: diag Aᴴ = star (diag A).

LaTeX

$$$\\operatorname{diag}(A)^{\\mathsf{H}} = \\operatorname{diag}(A^{\\star})$$$

Lean4

@[simp]
theorem diagonal_conjTranspose [AddMonoid α] [StarAddMonoid α] (v : n → α) : (diagonal v)ᴴ = diagonal (star v) :=
  by
  rw [conjTranspose, diagonal_transpose, diagonal_map (star_zero _)]
  rfl

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