nonsing_inv_eq_ringInverse — Mathlib

English

The nonsingular inverse equals Ring.inverse A for any A, after case analysis on det.

Русский

Несингобратная обратная матрица совпадает с Ring.inverse A после анализа det.

LaTeX

$$$A^{-1} = \\operatorname{Ring.inverse}(A)$$$

Lean4

/-- The nonsingular inverse is the same as the general `Ring.inverse`. -/
theorem nonsing_inv_eq_ringInverse : A⁻¹ = Ring.inverse A :=
  by
  by_cases h_det : IsUnit A.det
  · cases (A.isUnit_iff_isUnit_det.mpr h_det).nonempty_invertible
    rw [← invOf_eq_nonsing_inv, Ring.inverse_invertible]
  · have h := mt A.isUnit_iff_isUnit_det.mp h_det
    rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit A h_det]

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