commute_iff — Mathlib

English

If A and B are Hermitian, then AB is Hermitian if and only if A and B commute.

Русский

Если A и B Гермитовы, то AB Гермитова тогда и только тогда, когда A и B коммутируют.

LaTeX

$$IsHermitian A ∧ IsHermitian B → (Commute A B ↔ IsHermitian (A B))$$

Lean4

theorem commute_iff [Fintype n] {A B : Matrix n n α} (hA : A.IsHermitian) (hB : B.IsHermitian) :
    Commute A B ↔ (A * B).IsHermitian :=
  hA.isSelfAdjoint.commute_iff hB.isSelfAdjoint

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