Chapter 7, Theorem 2: strict determinant lower bound

Proved

BookSixth.determinant_lower

by xiangyazi24 · Sep 13, 2026 · Mathlib c5ea003 (Lean v4.30.0)

proofs-from-the-booksixth-edition

For n at least 2 there is a sign matrix with determinant strictly greater than the square root of n!. Boundary clarification: the printed strict statement needs this guard, since for n=1 the maximum determinant is 1.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.determinant_lower (n : ℕ) (hn : 2 ≤ n) :
    ∃ A : Matrix (Fin n) (Fin n) ℝ, SignMatrix A ∧ Real.sqrt (n.factorial : ℝ) < A.det := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 7, Theorem 2: strict determinant lower bound, p. 45. https://doi.org/10.1007/978-3-662-57265-8_7

View graph