isHermitian_add_transpose_self — Mathlib

English

Let A be a square matrix over a ring with an involutive star. Then A + A* is Hermitian.

Русский

Пусть A — квадратная матрица над кольцом с операцией сопряжения. Тогда A + A* является Гермитовой матрицей.

LaTeX

$$$(A^{\\ast} + A)^{\\ast} = A^{\\ast} + A$$$

Lean4

theorem isHermitian_add_transpose_self (A : Matrix n n α) : (A + Aᴴ).IsHermitian :=
  IsSelfAdjoint.add_star_self A

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