Latin squares and defining sets

Coordinates and symbols are labelled. A defining set specifies the symbols of a fixed Latin square on a finite set of cells. No unproved mathematical hypotheses are incorporated into these definitions.

@[reducible, inline]

abbrev LatinQuarter.Cell (n : ℕ) : Type

A labelled row-column position in an order-n square.

Equations

• LatinQuarter.Cell n = (Fin n × Fin n)

@[reducible, inline]

abbrev LatinQuarter.Square (n : ℕ) : Type

A symbol assignment to every labelled cell, before imposing the Latin condition.

Equations

• LatinQuarter.Square n = (Fin n → Fin n → Fin n)

def LatinQuarter.IsLatin {n : ℕ} (L : Square n) : Prop

Every row and column contains every symbol exactly once.

Equations

• LatinQuarter.IsLatin L = ((∀ (r : Fin n), Function.Bijective (L r)) ∧ ∀ (c : Fin n), Function.Bijective fun (r : Fin n) => L r c)

def LatinQuarter.Agrees {n : ℕ} (P : Finset (Cell n)) (L M : Square n) : Prop

The square M retains the clues that L gives on P.

Equations

• LatinQuarter.Agrees P L M = ∀ p ∈ P, M p.1 p.2 = L p.1 p.2

def LatinQuarter.IsDefining {n : ℕ} (P : Finset (Cell n)) (L : Square n) : Prop

The Latin square L is uniquely determined by its entries on P.

Equations

• LatinQuarter.IsDefining P L = (LatinQuarter.IsLatin L ∧ ∀ (M : LatinQuarter.Square n), LatinQuarter.IsLatin M → LatinQuarter.Agrees P L M → M = L)

noncomputable def LatinQuarter.completions {n : ℕ} (P : Finset (Cell n)) (L : Square n) : Finset (Square n)

All labelled Latin squares extending the specified clues from L.

Equations

• LatinQuarter.completions P L = {M : LatinQuarter.Square n | LatinQuarter.IsLatin M ∧ LatinQuarter.Agrees P L M}

@[simp]

theorem LatinQuarter.mem_completions {n : ℕ} {P : Finset (Cell n)} {L M : Square n} : M ∈ completions P L ↔ IsLatin M ∧ Agrees P L M

theorem LatinQuarter.defining_iff_completions_eq_singleton {n : ℕ} (P : Finset (Cell n)) (L : Square n) : IsDefining P L ↔ completions P L = {L}

theorem LatinQuarter.defining_completion_count {n : ℕ} {P : Finset (Cell n)} {L : Square n} (h : IsDefining P L) : (completions P L).card = 1