isDiag_conjTranspose_iff — Mathlib

English

Aᴴ.IsDiag ↔ A.IsDiag for a NonUnitalNonAssocSemiring with StarRing; the property is symmetric.

Русский

Aᴴ.IsDiag эквивалентно A.IsDiag и обратно.

LaTeX

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

Lean4

@[simp]
theorem isDiag_conjTranspose_iff [NonUnitalNonAssocSemiring α] [StarRing α] {A : Matrix n n α} : Aᴴ.IsDiag ↔ A.IsDiag :=
  ⟨fun ha => by
    convert ha.conjTranspose
    simp, IsDiag.conjTranspose⟩

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