Chapter 7, Equation (5): determinant bound

Proved

BookSixth.hadamard_bound

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

proofs-from-the-booksixth-edition

For a positive order n and a real sign matrix A, the absolute determinant is at most n raised to the real power n/2.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.hadamard_bound {n : ℕ} (hn : 0 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A) :
    |A.det| ≤ (n : ℝ) ^ ((n : ℝ) / 2) := by sorry

Source

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

View graph