Adjugate

Cofactor expansion, the adjugate identity, and determinant annihilation (ZF)

Open in Workbench View on GitHub

1-- Cofactor expansion, the adjugate identity, and determinant annihilation (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 AdjugateExample7import Grace.Cumulus.Algebra.Ring.DeterminantKernel89section Rings10variable (A add zero neg mul one : Set)11notation ring R := (A, add, zero, neg, mul, one)12hypothesis ring : IsCommRing(R)1314theorem diagonal (n : Nat) (M i : Set)15  requires matrix : RingMatrix(n, R, M)16  requires row : i ∈ n17  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, i) = determinant(n, R, M)18proof19  exact adjugate.right_diagonal with *2021theorem off_diagonal (n : Nat) (M i j : Set)22  requires matrix : RingMatrix(n, R, M)23  requires row : i ∈ n24  requires column : j ∈ n25  requires distinct : i ≠ j26  shows matrixProductEntry(n, R, M, adjugate(n, R, M), i, j) = R[0]27proof28  exact adjugate.right_off_diagonal with *2930theorem annihilate (n : Nat) (M v j : Set)31  requires matrix : RingMatrix(n, R, M)32  requires kernel : LeftKernelVector(n, R, M, v)33  requires index : j ∈ n34  shows determinant(n, R, M) * v(j) = R[0]35proof36  exact determinant.annihilates_left_kernel with *3738-- Over a domain, a nonzero kernel coordinate forces the determinant to vanish.39theorem singular (n : Nat) (M v j : Set)40  requires domain : IsIntegralDomain(R)41  requires matrix : RingMatrix(n, R, M)42  requires kernel : LeftKernelVector(n, R, M, v)43  requires index : j ∈ n44  requires nonzero : v(j) ≠ R[0]45  shows determinant(n, R, M) = R[0]46proof47  exact determinant.zero_of_nonzero_left_kernel with *4849end Rings50