isHermitian_mul_mul_conjTranspose

English

If A is Hermitian, then B^H A B is Hermitian for any B.

Русский

Если A Гермитова, то B^H A B Гермитова для любого B.

LaTeX

$$$(B^{\\mathrm{H}} A B)^{\\mathrm{H}} = B^{\\mathrm{H}} A B$$$

Lean4

/-- Note this is more general than `IsSelfAdjoint.conjugate` as `B` can be rectangular. -/
theorem isHermitian_mul_mul_conjTranspose [Fintype m] {A : Matrix m m α} (B : Matrix n m α) (hA : A.IsHermitian) :
    (B * A * Bᴴ).IsHermitian := by
  simp only [IsHermitian, conjTranspose_mul, conjTranspose_conjTranspose, hA.eq, Matrix.mul_assoc]

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