DeterminantRows

Familiar row operations, stated only through their matrix entries (ZF)

Open in Workbench View on GitHub

1-- Familiar row operations, stated only through their matrix entries (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 DeterminantRows7import Grace.Cumulus.Algebra.Ring.DeterminantRows89section Rings10variable (A add zero neg mul one : Set)11notation ring R := (A, add, zero, neg, mul, one)12hypothesis ring : IsCommRing(R)1314theorem add_row (n : Nat) (M N i r a : Set)15  requires matrixM : RingMatrix(n, R, M)16  requires matrixN : RingMatrix(n, R, N)17  requires row : i ∈ n18  requires source : r ∈ n19  requires distinct : i ≠ r20  requires scalar : a ∈ R21  requires outside : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, N[k, j] = M[k, j]22  requires entries : ∀ j ∈ n, N[i, j] = M[i, j] + a * M[r, j]23  shows determinant(n, R, N) = determinant(n, R, M)24proof25  exact determinant.row_add_multiple with *2627theorem scale_row (n : Nat) (M N i a : Set)28  requires matrixM : RingMatrix(n, R, M)29  requires matrixN : RingMatrix(n, R, N)30  requires row : i ∈ n31  requires scalar : a ∈ R32  requires outside : ∀ k ∈ n, k ≠ i → ∀ j ∈ n, N[k, j] = M[k, j]33  requires entries : ∀ j ∈ n, N[i, j] = a * M[i, j]34  shows determinant(n, R, N) = a * determinant(n, R, M)35proof36  exact determinant.row_scale with *3738end Rings39