Chapter 7, Hadamard order restriction

Proved

BookSixth.hadamard_order

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

proofs-from-the-booksixth-edition

A real sign matrix of order n greater than 2 with orthogonal columns must have order divisible by 4.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.hadamard_order {n : ℕ} (hn : 2 < n) (A : Matrix (Fin n) (Fin n) ℝ) (hA : SignMatrix A) (horth : A.transpose * A = (n : ℝ) • (1 : Matrix (Fin n) (Fin n) ℝ)) :
    4 ∣ n := by sorry

Source

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

View graph