mkOfDetNeZero — Mathlib

English

If A has nonzero determinant over a field, then A ∈ GL_n(K).

Русский

Если детерминант матрицы A не ноль, то A ∈ GL_n(K).

LaTeX

$$def mkOfDetNeZero {K} [Field K] (A : Matrix n n K) (h : Matrix.det A ≠ 0) : GL n K$$

Lean4

/-- Given a matrix with non-zero determinant over a field, we get an element of `GL n K`. -/
@[simps! val]
def mkOfDetNeZero {K : Type*} [Field K] (A : Matrix n n K) (h : Matrix.det A ≠ 0) : GL n K :=
  mk' A (invertibleOfNonzero h)

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