PermutationSigns

Actual inversion-count signs and equal-row determinant cancellation (ZF)

Open in Workbench View on GitHub

1-- Actual inversion-count signs and equal-row determinant cancellation (ZF).2-- Copyright (c) 2026 Grant Passmore.3-- Released under the Apache License 2.0. See LICENSE in the repository root.4-- Authors: Grant Passmore56module PermutationSigns7import Grace.Cumulus.Algebra.Ring.PermutationSign89section Rings10variable (A add zero neg mul one : Set)11notation ring R := (A, add, zero, neg, mul, one)12hypothesis ring : IsCommRing(R)1314theorem exchange_reverses_sign (n : Nat) (a b p : Set)15  requires ha : a ∈ n16  requires hb : b ∈ n17  requires distinct : a ≠ b18  requires permutation : p ∈ permutations(n)19  shows permutationSign(n, A, add, zero, neg, mul, one, permutationExchange(n, a, b)(p)) = R[-permutationSign(n, A, add, zero, neg, mul, one, p)]20proof21  exact permutationSign.exchange with *2223theorem equal_rows_vanish (n : Nat) (a b M : Set)24  requires matrix : RingMatrix(n, R, M)25  requires ha : a ∈ n26  requires hb : b ∈ n27  requires distinct : a ≠ b28  requires rows : ∀ j ∈ n, M[a, j] = M[b, j]29  shows determinant(n, R, M) = R[0]30proof31  exact determinant.equal_rows with *3233end Rings3435theorem fresh_insertion_counts (S a : Set)36  requires finite : Finite(S)37  requires fresh : ¬(a ∈ S)38  shows cardinality(insert(a, S)) = succ(cardinality(S))39proof40  exact cardinality.insert with *41