Determinants

General finite determinants and multiplication-row selection, without Choice

Open in Workbench View on GitHub

1-- General finite determinants and multiplication-row selection, without Choice.2-- Part of the Grace17 examples.3-- Copyright (c) 2026 Grant Passmore.4-- Released under the Apache License 2.0. See LICENSE in the repository root.5-- Authors: Grant Passmore67module Determinants8import Grace.Cumulus.Algebra.CoefficientMatrix9import Grace.Cumulus.Algebra.Ring.DeterminantZero1011section Rings12variable (A add zero neg mul one M : Set)13notation ring R := (A, add, zero, neg, mul, one)14hypothesis ring : IsCommRing(R)1516theorem value_is_in_ring (n : Nat)17  requires matrix : RingMatrix(n, R, M)18  shows determinant(n, R, M) ∈ R19proof20  exact determinant.closed with *2122theorem empty_determinant23  requires matrix : RingMatrix(∅, R, M)24  shows determinant(∅, R, M) = R[1]25proof26  exact determinant.empty with *2728theorem equal_entries (n : Nat) (N : Set)29  requires matrix : RingMatrix(n, R, M)30  requires other : RingMatrix(n, R, N)31  requires entries : ∀ i ∈ n, ∀ j ∈ n, M[i, j] = N[i, j]32  shows determinant(n, R, M) = determinant(n, R, N)33proof34  exact determinant.congr with *3536theorem zero_row (n : Nat) (i : Set)37  requires matrix : RingMatrix(n, R, M)38  requires row : i ∈ n39  requires vanishes : ∀ j ∈ n, M[i, j] = R[0]40  shows determinant(n, R, M) = R[0]41proof42  exact determinant.zero_row with *4344end Rings4546section Algebras47variable (A add zero neg mul one B plus z minus times unit f x : Set)48notation ring R := (A, add, zero, neg, mul, one)49notation ring S := (B, plus, z, minus, times, unit)50hypothesis source : IsCommRing(R)51hypothesis target : IsCommRing(S)52hypothesis hom : IsRingHom(f, R, S)53hypothesis element : x ∈ S5455theorem select_all_multiplication_rows56  requires finiteModule : FiniteAlgebraModule(f, R, S)57  shows ∃ xs, List(B, xs) ∧ linearSpan(f, R, S, listSupport{B}(xs)) = S ∧58    (∃ C, Finite(C) ∧ (∀ cs ∈ C, List(A, cs) ∧ ListOps.length{A}(cs) = ListOps.length{B}(xs)) ∧59      (∃ rows, FunctionBetween(rows, listSupport{B}(xs), C) ∧60        (∀ g ∈ listSupport{B}(xs), S[x * g] = linearCombination(R, S, f, xs, rows(g)))))61proof62  exact FiniteAlgebraModule.multiplication_rows with *6364end Algebras65