coe_units_inv — Mathlib

English

The coercion of the inverse of a unit matrix equals the nonsingular inverse.

Русский

Сведение обратной единицы матрицы к обычной матрице совпадает с несинговой обратной.

LaTeX

$$$\\uparrow (U^{-1}) = U^{-1}_{\\mathrm{ns}}$ for all $U \\in \\mathrm{Matrix}_n(\\alpha)^{\\times}$$$

Lean4

/-- Coercing the result of `Units.instInv` is the same as coercing first and applying the
nonsingular inverse. -/
@[simp, norm_cast]
theorem coe_units_inv (A : (Matrix n n α)ˣ) : ↑A⁻¹ = (A⁻¹ : Matrix n n α) :=
  by
  letI := A.invertible
  rw [← invOf_eq_nonsing_inv, invOf_units]

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