English
There is a computable (Decidable) instance for the relation that identifies when two permutations of α differ by a single swap, on a finite type α.
Русский
Существует вычислимая (решимая) инстанция для отношения между перестановками α на конечном множестве, которое различает две перестановки по одному обмену.
LaTeX
$$$ \\forall α\\, [Fintype α], \\; (i,j) \\mapsto (\\mathrm{modSwap}\\, i\\, j) \\.\\mathrm{r} $ is a decidable relation$$
Lean4
/-- `modSwap i j` contains permutations up to swapping `i` and `j`.
We use this to partition permutations in `Matrix.det_zero_of_row_eq`, such that each partition
sums up to `0`.
-/
def modSwap (i j : α) : Setoid (Perm α) :=
⟨fun σ τ => σ = τ ∨ σ = swap i j * τ, fun σ => Or.inl (refl σ), fun {σ τ} h =>
Or.casesOn h (fun h => Or.inl h.symm) fun h => Or.inr (by rw [h, swap_mul_self_mul]), fun {σ τ υ} hστ hτυ => by
rcases hστ with hστ | hστ <;> rcases hτυ with hτυ | hτυ <;> (try rw [hστ, hτυ, swap_mul_self_mul]) <;>
simp [hστ, hτυ]⟩
