det_nonsing_inv — Mathlib

English

If det A is a unit, then det(A⁻¹) = Ring.inverse(det A).

Русский

Если детерминант A единичен, то det(A⁻¹) = Ring.inverse(det A).

LaTeX

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

Lean4

@[simp]
theorem det_nonsing_inv : A⁻¹.det = Ring.inverse A.det :=
  by
  by_cases h : IsUnit A.det
  · cases h.nonempty_invertible
    letI := invertibleOfDetInvertible A
    rw [Ring.inverse_invertible, ← invOf_eq_nonsing_inv, det_invOf]
  cases isEmpty_or_nonempty n
  · rw [det_isEmpty, det_isEmpty, Ring.inverse_one]
  · rw [Ring.inverse_non_unit _ h, nonsing_inv_apply_not_isUnit _ h, det_zero ‹_›]

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