isHermitian_conjTranspose_mul_mul

English

If hA is Hermitian, then -A is Hermitian.

Русский

Если A Гермитова, то -A Герметова.

LaTeX

$$$A^{\\mathrm{H}} = A \\Rightarrow (-A)^{\\mathrm{H}} = -A$$$

Lean4

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

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