isHermitian_inv — Mathlib

English

For Hermitian A, A^{-1} is Hermitian if and only if A is Hermitian.

Русский

Для Гермитовой A обратная A^{-1} Гермитова тогда и только тогда, когда A Гермитова.

LaTeX

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

Lean4

@[simp]
theorem isHermitian_inv [Fintype m] [DecidableEq m] (A : Matrix m m α) [Invertible A] :
    A⁻¹.IsHermitian ↔ A.IsHermitian :=
  ⟨fun h => by rw [← inv_inv_of_invertible A]; exact IsHermitian.inv h, IsHermitian.inv⟩

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