structure LatinSquare (n : ℕ) : Type

A latin square of order n is an n × n matrix with entries in Fin n such that each symbol appears exactly once in every row and exactly once in every column.

• mat : Matrix (Fin n) (Fin n) (Fin n)
• row_injective (i : Fin n) : Function.Injective (self.mat i)

  Each row is a permutation of Fin n.

• col_injective (j : Fin n) : Function.Injective (self.mat.transpose j)

  Each column is a permutation of Fin n.

instance instFintypeLatinSquare {n : ℕ} : Fintype (LatinSquare n)

There are finitely many latin squares of order n, since each is determined by a matrix in the finite type Matrix (Fin n) (Fin n) (Fin n). This is useful for defining the maximum number of transversals over all latin squares of order n.

Equations

• One or more equations did not get rendered due to their size.

@[reducible, inline]

abbrev IsTransversal {n : ℕ} (L : LatinSquare n) (σ : Fin n → Fin n) : Prop

A transversal of a latin square L is a selection of one cell per row, given by a column-selector σ, such that the selected columns are all distinct and the symbols at the selected cells are all distinct.

Equations

• IsTransversal L σ = (Function.Injective σ ∧ Function.Injective fun (i : Fin n) => L.mat i (σ i))

@[reducible, inline]

abbrev IsNearTransversal {n : ℕ} (L : LatinSquare n) (ρ σ : Fin (n - 1) → Fin n) : Prop

A near-transversal of a latin square L of order n is a selection of n - 1 cells, given by a row-selector ρ and a column-selector σ (both Fin (n - 1) → Fin n), such that the selected rows are all distinct, the selected columns are all distinct, and the symbols at the selected cells are all distinct.

Equations

• IsNearTransversal L ρ σ = (Function.Injective ρ ∧ Function.Injective σ ∧ Function.Injective fun (i : Fin (n - 1)) => L.mat (ρ i) (σ i))

def numTransversals {n : ℕ} (L : LatinSquare n) : ℕ

The number of transversals of a latin square L, defined as the cardinality of the type of column-selectors σ : Fin n → Fin n satisfying IsTransversal L σ.

Equations

• numTransversals L = Fintype.card { σ : Fin n → Fin n // IsTransversal L σ }