Chapter 7, Powers-of-two construction

Proved

BookSixth.sylvester

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

proofs-from-the-booksixth-edition

For every nonnegative integer m, there is a real Hadamard matrix of order 2^m, including order one.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.sylvester (m : ℕ) :
    ∃ A : Matrix (Fin (2^m)) (Fin (2^m)) ℝ, SignMatrix A ∧
      A.transpose * A = ((2^m : ℕ) : ℝ) • (1 : Matrix (Fin (2^m)) (Fin (2^m)) ℝ) := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 7, Powers-of-two construction, p. 44. https://doi.org/10.1007/978-3-662-57265-8_7

View graph