unitOfDetInvertible — Mathlib

English

Given a proof that det A is invertible, one can lift A to a unit (an invertible matrix) in the matrix ring.

Русский

Если дано доказательство обратимости det(A), можно поднять A до единицы (обратимой матрицы) в кольце матриц.

LaTeX

$$def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ$$

Lean4

/-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(Matrix n n α)ˣ` -/
def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ :=
  @unitOfInvertible _ _ A (invertibleOfDetInvertible A)

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