Nonsingular exactly when the determinant is nonzero (Four.I.2)

Open

hefferon_nonsingular_iff_det_ne_zero

by tianyipeng · Aug 4, 2026 · Mathlib c5ea003 (Lean v4.30.0)

determinantinvertibilitylinear-algebra

An $n \times n$ matrix $A$ over a field $K$ has a two-sided inverse if and only if $\det A \neq 0$ .

Preamble

import Mathlib.Data.Matrix.Basic
import Mathlib.LinearAlgebra.Matrix.NonsingularInverse
import Mathlib.LinearAlgebra.Matrix.ToLin

open Matrix

Formal statement

theorem hefferon_nonsingular_iff_det_ne_zero
    {K : Type*} [Field K] {n : ℕ} (A : Matrix (Fin n) (Fin n) K) :
    (∃ B : Matrix (Fin n) (Fin n) K, A * B = 1 ∧ B * A = 1) ↔ A.det ≠ 0 := by
  sorry

Source

Jim Hefferon, *Linear Algebra*, Saint Michael's College, 2020 printing, Chapter Four, Section I.2, Theorem 2.5, p. 344

View graph