theorem Hex.Perm.Cycle.sign_formPerm {n : ℕ} (xs : List (Fin n)) (h : xs.Nodup) : ↑(Equiv.Perm.sign xs.formPerm) = (-1) ^ (xs.length - 1)

theorem Hex.Perm.Cycle.sign_prod {n : ℕ} (cs : List (Array (Fin n))) (hd : ∀ c ∈ cs, c.toList.Nodup) : ↑(Equiv.Perm.sign (List.map (fun (c : Array (Fin n)) => c.toList.formPerm) cs).prod) = (-1) ^ (List.map (fun (c : Array (Fin n)) => c.size - 1) cs).sum

theorem Hex.Perm.Cycle.sum_defect {n : ℕ} (cs : List (Array (Fin n))) (hc : ∀ c ∈ cs, 0 < c.size) : (List.map (fun (c : Array (Fin n)) => c.size - 1) cs).sum + cs.length = (List.map Array.size cs).sum

theorem Hex.Perm.sign_pow {n : ℕ} (p : Perm n) : p.sign = (-1) ^ (n - p.allCycles.size)

theorem Hex.Perm.sign_eq_mathlib {n : ℕ} (p : Perm n) : p.sign = ↑(Equiv.Perm.sign p.toEquiv)

The executable cycle-count formula agrees with Mathlib's sign homomorphism.

theorem Hex.Perm.sign_comp {n : ℕ} (p q : Perm n) : (p.comp q).sign = p.sign * q.sign

@[simp]

theorem Hex.Perm.sign_id {n : ℕ} : (Perm.id n).sign = 1

@[simp]

theorem Hex.Perm.sign_inv {n : ℕ} (p : Perm n) : p.inv.sign = p.sign

theorem Hex.Perm.sign_transpositions {n : ℕ} (p : Perm n) (xs : List (Perm n)) (hs : ∀ q ∈ xs, Equiv.Perm.IsSwap q.toEquiv) (hp : (List.map toEquiv xs).prod = p.toEquiv) : p.sign = (-1) ^ xs.length

Every decomposition into transpositions gives the same parity as the executable cycle-count formula.