lean_workbook_plus_34790

Open

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Construct a matrix with integer coefficients and non-zero determinant, not necessarily $\pm1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34790 : ∃ A : Matrix (Fin 2) (Fin 2) ℤ, A.det ≠ 0   :=  by sorry

Source