Chapter 37, Theorem 2: Latin square count

Proved

BookSixth.latin_bounds

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

proofs-from-the-booksixth-edition

For positive n, the number L(n) of labeled Latin squares on a fixed n-symbol alphabet is between (n!)^(2n)/n^(n²) and the product from k=1 to n of (k!)^(n/k). The latter exponents are real.

Preamble

import Mathlib
import Definitions.Def_BookSixth
open scoped BigOperators
open BookSixth

Formal statement

theorem BookSixth.latin_bounds (n : ℕ) (hn : 0 < n) :
    ((n.factorial : ℝ) ^ (2*n) / (n : ℝ) ^ (n*n) ≤ latinCount n) ∧
      ((latinCount n : ℝ) ≤ ∏ k ∈ Finset.Icc 1 n,
        (k.factorial : ℝ) ^ ((n : ℝ) / (k : ℝ))) := by sorry

Source

Aigner and Ziegler, Proofs from THE BOOK, Sixth Edition (2018), Chapter 37, Theorem 2: Latin square count, p. 266. https://doi.org/10.1007/978-3-662-57265-8_37

View graph