conjTranspose — Mathlib

English

If A is diagonal, then its conjugate transpose Aᴴ is diagonal (for a star ring).

Русский

Если A диагональная, то Aᴴ диагональна (при звёздном кольце).

LaTeX

$$$\\forall {\\alpha} [NonUnitalNonAssocSemiring \\alpha] [StarRing \\alpha] {A : Matrix n n \\alpha}, A.IsDiag \\to Aᴴ.IsDiag$$$

Lean4

theorem conjTranspose [NonUnitalNonAssocSemiring α] [StarRing α] {A : Matrix n n α} (ha : A.IsDiag) : Aᴴ.IsDiag :=
  ha.transpose.map (star_zero _)

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