structure LatinSquares.IsLatinSquare {n : ℕ} (L : Fin n → Fin n → Fin n) : Prop

An $n \times n$ array $L : \text{Fin}\ n \to \text{Fin}\ n \to \text{Fin}\ n$ is a Latin square if every row and every column is a permutation of $\{0,1,\dots,n-1\}$, equivalently if every row map and every column map is injective.

• row_injective (i : Fin n) : Function.Injective (L i)
• col_injective (j : Fin n) : Function.Injective fun (i : Fin n) => L i j

def LatinSquares.HasLatinTransversal {n : ℕ} (L : Fin n → Fin n → Fin n) : Prop

An $n \times n$ array $L$ has a Latin transversal if there exists a permutation $\sigma$ of $\text{Fin}\ n$ such that the diagonal entries $L_{i,\sigma(i)}$ are all distinct.

theorem ryser_conjecture {n : ℕ} (hn : Odd n) (L : Fin n → Fin n → Fin n) (hL : LatinSquares.IsLatinSquare L) : LatinSquares.HasLatinTransversal L

Ryser's conjecture: every $n \times n$ Latin square with $n$ odd has a Latin transversal.

noncomputable def LatinSquares.transversalSymbols {n : ℕ} (L : Fin n → Fin n → Fin n) (σ : Equiv.Perm (Fin n)) : Finset (Fin n)

The set of symbols appearing on the diagonal selected by the permutation $\sigma$, i.e. $\{L_{i,\sigma(i)} : i \in \text{Fin}\ n\}$.

theorem ryser_brualdi_stein_conjecture {n : ℕ} {L : Fin n → Fin n → Fin n} (hL : LatinSquares.IsLatinSquare L) (hn : Even n) : ∃ (σ : Equiv.Perm (Fin n)), n - 1 ≤ (LatinSquares.transversalSymbols L σ).card

Ryser–Brualdi–Stein conjecture: every $n \times n$ Latin square with $n$ even admits a permutation $\sigma$ such that the diagonal $\{L_{i,\sigma(i)}\}$ contains at least $n-1$ distinct symbols (a near-transversal).

def ErdosSpencer.symbolCount {n : ℕ} {α : Type u_1} [DecidableEq α] (L : Fin n → Fin n → α) (c : α) : ℕ

The number of cells of the array $L$ whose entry equals the symbol $c$, i.e. $|\{(i,j) : L_{i,j} = c\}|$.

def ErdosSpencer.HasLatinTransversalGen {n : ℕ} {α : Type u_1} (L : Fin n → Fin n → α) : Prop

Generalised notion of a Latin transversal for an array with entries in an arbitrary type $\alpha$: a permutation $\sigma$ such that the selected diagonal entries $L_{i,\sigma(i)}$ are all distinct.

def ErdosSpencer.goodPerms {n : ℕ} {α : Type u_1} [DecidableEq α] (L : Fin n → Fin n → α) : Finset (Equiv.Perm (Fin n))

The finite set of permutations $\sigma$ that yield a Latin transversal of $L$: distinct rows pick distinct symbols.

theorem ErdosSpencer.mem_goodPerms_iff {n : ℕ} {α : Type u_1} [DecidableEq α] (L : Fin n → Fin n → α) (σ : Equiv.Perm (Fin n)) : σ ∈ goodPerms L ↔ Function.Injective fun (i : Fin n) => L i (σ i)

Membership in goodPerms L is equivalent to the diagonal map $i \mapsto L_{i,\sigma(i)}$ being injective.

theorem ErdosSpencer.lll_latin_transversal_nonempty {n : ℕ} {α : Type u_1} [DecidableEq α] (hn : 2 ≤ n) (L : Fin n → Fin n → α) (hL : ∀ (c : α), ↑(symbolCount L c) ≤ ↑n / (4 * Real.exp 1)) : (goodPerms L).Nonempty

Lopsided LLL application underlying Erdős–Spencer: for $n \ge 2$, if every symbol of the $n \times n$ array $L$ appears at most $n/(4e)$ times, then the set of permutations producing a Latin transversal is nonempty.

theorem ErdosSpencer.erdos_spencer_latin_transversal {n : ℕ} {α : Type u_1} [DecidableEq α] (hn : 0 < n) (L : Fin n → Fin n → α) (hL : ∀ (c : α), ↑(symbolCount L c) ≤ ↑n / (4 * Real.exp 1)) : HasLatinTransversalGen L

Erdős–Spencer 1991 (Theorem 6.5.11): if $L$ is an $n \times n$ array (with $n \ge 1$) in which every symbol appears at most $n/(4e)$ times, then $L$ has a Latin transversal.