Chapter 7, Equation (6): equality case

Proved

BookSixth.hadamard_equality

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

proofs-from-the-booksixth-edition

A positive-order sign matrix attains the Hadamard determinant bound if and only if its distinct columns are orthogonal.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.hadamard_equality {n : ℕ} (hn : 0 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A) :
    (|A.det| = (n : ℝ) ^ ((n : ℝ) / 2)) ↔
      ∀ i j, i ≠ j → (∑ k, A k i * A k j) = 0 := by sorry

Source

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

View graph