mul_nonsing_inv — Mathlib

English

Over a StarRing α, A⁻¹ᴴ = Aᴴ⁻¹, i.e., conjugate-transpose preserves inverse.

Русский

В звездной кольце α сопряженная транспонированная сохраняет обратную: A⁻¹ᴴ = Aᴴ⁻¹.

LaTeX

$$$A^{-1\,*} = (A^{*})^{-1}$$$

Lean4

/-- The `nonsing_inv` of `A` is a right inverse. -/
@[simp]
theorem mul_nonsing_inv (h : IsUnit A.det) : A * A⁻¹ = 1 :=
  by
  cases (A.isUnit_iff_isUnit_det.mpr h).nonempty_invertible
  rw [← invOf_eq_nonsing_inv, mul_invOf_self]

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