invertibleOfIsUnitDet — Mathlib

English

Given [Invertible det(A)], A is invertible with A⁻¹ as the inverse.

Русский

Пусть det(A) является единицей; тогда A обратима и A⁻¹ — обратная к A.

LaTeX

$$$[Invertible\ det(A)] \Rightarrow Invertible\ A$ with inverse A⁻¹.$$

Lean4

/-- A version of `Matrix.invertibleOfDetInvertible` with the inverse defeq to `A⁻¹` that is
therefore noncomputable. -/
noncomputable def invertibleOfIsUnitDet (h : IsUnit A.det) : Invertible A :=
  ⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩

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