Chapter 7, Mean-square determinant identity

Proved

BookSixth.determinant_mean_square

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

proofs-from-the-booksixth-edition

Summing the squared determinants over all sign matrices of order n gives 2^(n²) n!, equivalently the uniform mean square is n!. Order zero is included.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.determinant_mean_square (n : ℕ) :
    (∑ B : Fin n → Fin n → Bool, (Matrix.det (fun i j => if B i j then (1 : ℝ) else -1))^2) = (2 : ℝ)^(n*n) * (n.factorial : ℝ) := by sorry

Source

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

View graph