Grace/Cumulus/Algebra/Ring/DeterminantRows.g17

Open in Workbench Download source

Imports

DeterminantLinearity · MatrixRows · PermutationSign

Declarations

• determinant.row_scale theorem derivation
• determinant.row_add_multiple theorem derivation

Source

1-- Elementary row operations preserve the determinant over any commutative ring (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 Grace.Cumulus.Algebra.Ring.DeterminantRows8import DeterminantLinearity9import MatrixRows10import PermutationSign1112section Rings13variable (A add zero neg mul one : Set)14notation ring R := (A, add, zero, neg, mul, one)15hypothesis ring : IsCommRing(R)1617theorem determinant.row_scale (n : Nat) (M N i a : Set)18  requires matrixM : RingMatrix(n, R, M)19  requires matrixN : RingMatrix(n, R, N)20  requires row : i ∈ n21  requires scalar : a ∈ R22  requires outside : ∀ k ∈ n, ¬(k = i) → ∀ j ∈ n, N[k, j] = M[k, j]23  requires entries : ∀ j ∈ n, N[i, j] = a * M[i, j]24  shows determinant(n, R, N) = a * determinant(n, R, M)25proof26  have zeroIn : R[0] ∈ R by typecheck27  have unchanged : ∀ k ∈ n, ¬(k = i) → ∀ j ∈ n, M[k, j] = M[k, j]28    intros k hk distinct j hj29    rfl30  have linear : ∀ j ∈ n, N[i, j] = a * M[i, j] + R[0] * M[i, j]31    intros j hj32    have closed := RingMatrix.entry at n, A, M, i, j with *33    have entry := entries with j, hj34    rw entry35    ring36  have equation := determinant.row_linear with *37  have closed := determinant.closed at A, add, zero, neg, mul, one, M, n with *38  rw equation39  ring4041-- No auxiliary matrix, coefficient graph, division, or nonzero scalar is42-- required from the caller: just the equations describing the row operation.43theorem determinant.row_add_multiple (n : Nat) (M N i r a : Set)44  requires matrixM : RingMatrix(n, R, M)45  requires matrixN : RingMatrix(n, R, N)46  requires row : i ∈ n47  requires source : r ∈ n48  requires distinct : i ≠ r49  requires scalar : a ∈ R50  requires outside : ∀ k ∈ n, ¬(k = i) → ∀ j ∈ n, N[k, j] = M[k, j]51  requires entries : ∀ j ∈ n, N[i, j] = M[i, j] + a * M[r, j]52  shows determinant(n, R, N) = determinant(n, R, M)53proof54  have copied := matrixCopyRow.matrix at n, A, M, i, r with *55  have unit : R[1] ∈ R by typecheck56  have reverse : r ≠ i57    intro equal58    apply distinct59    cc60  have outsideCopy : ∀ k ∈ n, ¬(k = i) → ∀ j ∈ n, matrixCopyRow(n, A, M, i, r)[k, j] = M[k, j]61    intros k hk different j hj62    exact matrixCopyRow.other with *63  have equalRows : ∀ j ∈ n, matrixCopyRow(n, A, M, i, r)[i, j] = matrixCopyRow(n, A, M, i, r)[r, j]64    intros j hj65    have left := matrixCopyRow.same at n, A, M, i, r, j with *66    have right := matrixCopyRow.other at n, A, M, i, r, r, j with *67    cc68  have vanishes := determinant.equal_rows with *69  have linear : ∀ j ∈ n, N[i, j] = R[1] * M[i, j] + a * matrixCopyRow(n, A, M, i, r)[i, j]70    intros j hj71    have value := matrixCopyRow.same at n, A, M, i, r, j with *72    have original := RingMatrix.entry at n, A, M, i, j with *73    have sourceEntry := RingMatrix.entry at n, A, M, r, j with *74    have entry := entries with j, hj75    rw [value, entry]76    ring77  have equation := determinant.row_linear with *78  have closed := determinant.closed at A, add, zero, neg, mul, one, M, n with *79  rw [equation, vanishes]80  ring8182end Rings83