DoubleSums

Interchange arbitrary finite rectangular sums and transpose twice (ZF)

Open in Workbench View on GitHub

1-- Interchange arbitrary finite rectangular sums and transpose twice (ZF).2-- Part of Cumulus, the Grace17 mathematics library.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module DoubleSums8import Grace.Cumulus.Algebra.Ring.DoubleSum910-- No fixed dimensions: both bounds may be any natural numbers, including zero.11theorem rows_equal_columns (A add zero neg mul one w : Set, m n : Nat)12  requires ring : IsCommRing(A, add, zero, neg, mul, one)13  requires matrix : w : m × n → A14  shows ringDoubleSum(w, add, zero, m, n) = ringDoubleSum(transposedMatrix(m, n, A, w), add, zero, n, m)15proof16  exact ringDoubleSum.interchange at A, add, zero, neg, mul, one, w, m, n with *1718theorem transpose_twice (D E A w : Set)19  requires matrix : w : D × E → A20  shows transposedMatrix(E, D, A, transposedMatrix(D, E, A, w)) = w21proof22  exact transposedMatrix.involution with matrix2324-- Independent local proofs may use the same names.25theorem local_witness_names (a : Set)26  requires inhabited : ∃ x, x = a27  shows a = a28proof29  simp30