def Hex.Matrix.permutationVectors (n : Nat) : List (Vector (Fin n) n)

Enumerate the permutations of Fin n as length-n vectors.

Equations

• One or more equations did not get rendered due to their size.
• Hex.Matrix.permutationVectors 0 = [#v[]]

def Hex.Matrix.inversionCount {n : Nat} : List (Fin n) → Nat

Count inversions in a permutation written as a list.

Equations

• Hex.Matrix.inversionCount [] = 0
• Hex.Matrix.inversionCount (x_1 :: xs) = List.foldl (fun (acc : Nat) (y : Fin n) => acc + if y < x_1 then 1 else 0) 0 xs + Hex.Matrix.inversionCount xs

theorem Hex.Matrix.permutationVectors_complete {n : Nat} {perm : Vector (Fin n) n} (hnodup : perm.toList.Nodup) : perm ∈ permutationVectors n

Every duplicate-free length-n vector of Fin n appears in permutationVectors n. This gives the completeness half of the local permutation enumeration used by the Leibniz determinant.

theorem Hex.Matrix.permutationVectors_nodup {n : Nat} {perm : Vector (Fin n) n} (hmem : perm ∈ permutationVectors n) : perm.toList.Nodup

Every vector enumerated by permutationVectors n is duplicate-free, so each listed vector really represents a permutation of Fin n.

theorem Hex.Matrix.permutationVectors_nodup_list {n : Nat} : (permutationVectors n).Nodup

The permutation enumeration itself has no duplicate vectors. This lets determinant proofs compare sums over permutationVectors by list permutation rather than by quotienting repeated terms.