FiniteSetSums

Enumeration-independent finite sums and single-index coefficient maps

Open in Workbench View on GitHub

1-- Enumeration-independent finite sums and single-index coefficient maps.2-- Part of the Grace17 proof assistant for mathematics based on set theory.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module FiniteSetSums8import Grace.Cumulus.Algebra.CoefficientSingle9import Grace.Cumulus.Algebra.Ring.FiniteSetSum1011section Sums12variable (V A add zero neg mul one w : Set)13hypothesis ring : IsCommRing(A, add, zero, neg, mul, one)14hypothesis weights : w : V → A15notation ring R := (A, add, zero, neg, mul, one)1617theorem enumeration_independent (f g : Set, n m : Nat)18  requires first : BijectiveBetween(f, n, V)19  requires second : BijectiveBetween(g, m, V)20  shows indexedRingSum(w, f, add, zero, n) = indexedRingSum(w, g, add, zero, m)21proof22  exact indexedRingSum.reindex at A, add, zero, neg, mul, one, w, V, f, g, n, m with *2324theorem evaluate_with_any_enumeration (f : Set, n : Nat)25  requires enumeration : BijectiveBetween(f, n, V)26  shows finiteRingSum(V, A, add, zero, neg, mul, one, w) = indexedRingSum(w, f, add, zero, n)27proof28  exact finiteRingSum.enumeration at V, A, add, zero, neg, mul, one, w, f, n with *2930theorem scalar_linearity (a : Set)31  requires finite : Finite(V)32  requires scalar : a ∈ A33  shows finiteRingSum(V, A, add, zero, neg, mul, one, coefficientScale(V, A, add, zero, neg, mul, one, a, w)) =34    a * finiteRingSum(V, A, add, zero, neg, mul, one, w)35proof36  exact finiteRingSum.scale with ring, finite, weights, scalar3738theorem single_nonzero_support (a j : Set)39  requires coefficient : a ∈ A40  requires index : j ∈ V41  requires nonzero : a ≠ zero42  shows functionSupport(coefficientSingle(V, A, zero, a, j), V, zero) = {j}43proof44  have ordinary := IsCommRing.ring with ring45  have zeroIn := IsRing.zero_in_carrier with ordinary46  exact coefficientSingle.support_nonzero with zeroIn, coefficient, index, nonzero4748end Sums49