Independent permutations of free row entries

@[reducible, inline]

abbrev LatinQuarter.FreeColumn {n : ℕ} (P : Finset (Cell n)) (r : Fin n) : Type

Columns whose entries in row r have not been specified as clues.

Equations

• LatinQuarter.FreeColumn P r = { c : Fin n // (r, c) ∉ P }

@[reducible, inline]

abbrev LatinQuarter.RowChoices {n : ℕ} (P : Finset (Cell n)) : Type

Independent permutations of the unfilled positions in each row.

Equations

• LatinQuarter.RowChoices P = ((r : Fin n) → Equiv.Perm (LatinQuarter.FreeColumn P r))

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

Permute the symbols of each row only within its unfilled cells.

Equations

• LatinQuarter.chosenSquare P L σ r c = L r (((σ r).subtypeCongr (Equiv.refl { a : Fin n // ¬(r, a) ∉ P })) c)

@[simp]

theorem LatinQuarter.chosenSquare_free {n : ℕ} (P : Finset (Cell n)) (L : Square n) (σ : RowChoices P) (r : Fin n) (c : FreeColumn P r) : chosenSquare P L σ r ↑c = L r ↑((σ r) c)

@[simp]

theorem LatinQuarter.chosenSquare_clue {n : ℕ} (P : Finset (Cell n)) (L : Square n) (σ : RowChoices P) (r c : Fin n) (hc : (r, c) ∈ P) : chosenSquare P L σ r c = L r c

@[simp]

theorem LatinQuarter.chosenSquare_one {n : ℕ} (P : Finset (Cell n)) (L : Square n) : chosenSquare P L 1 = L

theorem LatinQuarter.chosenSquare_rows {n : ℕ} (P : Finset (Cell n)) (L : Square n) (hL : IsLatin L) (σ : RowChoices P) (r : Fin n) : Function.Bijective (chosenSquare P L σ r)

theorem LatinQuarter.chosenSquare_agrees {n : ℕ} (P : Finset (Cell n)) (L : Square n) (σ : RowChoices P) : Agrees P L (chosenSquare P L σ)

theorem LatinQuarter.chosenSquare_injective {n : ℕ} (P : Finset (Cell n)) (L : Square n) (hL : IsLatin L) : Function.Injective (chosenSquare P L)

theorem LatinQuarter.unique_chosenSquare {n : ℕ} (P : Finset (Cell n)) (L : Square n) (h : IsDefining P L) (σ : RowChoices P) (hσ : IsLatin (chosenSquare P L σ)) : σ = 1

theorem LatinQuarter.det_eq_matching_sum {R : Type u_1} {ι : Type u_2} [CommRing R] [CharP R 2] [Fintype ι] [DecidableEq ι] (M : Matrix ι ι R) : M.det = ∑ σ : Equiv.Perm ι, ∏ i : ι, M i (σ i)

In characteristic two the determinant is exactly the unsigned matching sum, written with a choice in each selected row.