LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

The adjugate gives an explicit inverse formula over a field

Statement

Let $F$ be a field, $q \geq 1$ , and $M \in F^{q \times q}$ . Let $adj (M)$ be the adjugate defined by the cofactors of Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring. Then

M adj (M) = \det (M) I_{q} .

Consequently, when $\det (M) \neq 0$ , $M^{- 1} = adj (M) / \det (M)$ ; when $\det (M) = 0$ , $M$ is singular.

Facts & Assumptions

Given: A field $F$ , positive integer $q$ , and matrix $M \in F^{q \times q}$ .

[F1]

Deleted-row-and-column minors, cofactors, the cofactor matrix and the adjugate over a commutative ring: Rows and columns are indexed by $0, \dots, q - 1$ ; $C_{j k} (M) = (- 1)^{j + k} \det (M^{(j, k)})$ and $adj (M) = cof (M)^{T}$ , with the $0 \times 0$ determinant equal to $1$ when $q = 1$ .

[F2]

Laplace expansion computes the determinant along every row and every column over a commutative ring: With zero-based indices, expanding along row $j$ gives $\det (M) = \sum_{k = 0}^{q - 1} m_{j k} C_{j k} (M)$ .

[F3]

The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring: A determinant with two equal columns is zero. By For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$ , a determinant with two equal rows is also zero.

[F4]

A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero: A finite-dimensional linear operator over a field is invertible if and only if its determinant is nonzero.

Proof

1.1F1algebra

For $0 \leq i, j < q$ , [F1] makes the $(i, j)$ entry of $M adj (M)$ equal to $\sum_{k = 0}^{q - 1} m_{i k} C_{j k} (M)$ .

2.1F2F3step 1.1algebra

If $i = j$ , this sum is $\det (M)$ by [F2]. If $i \neq j$ , let $M^{'}$ be obtained by replacing row $j$ of $M$ with row $i$ . Deleting row $j$ leaves each cofactor unchanged, so expansion of $\det (M^{'})$ along row $j$ gives the sum in step 1.1. The matrix $M^{'}$ has equal rows $i$ and $j$ , so [F3] makes that determinant zero. Thus every diagonal entry of $M adj (M)$ is $\det (M)$ and every off-diagonal entry is zero.

3.1F4step 2.1algebra∎

If $\det (M) \neq 0$ , [F4] gives $M^{- 1}$ , and multiplying the identity in step 2.1 on the left by $M^{- 1} / \det (M)$ gives $adj (M) / \det (M) = M^{- 1}$ . If $\det (M) = 0$ , [F4] says $M$ is not invertible, which is exactly singularity for a square matrix.

Depends on

Used by

Dependency tree · two levels

19 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

MA1111 Linear Algebra I, Lecture 10: Determinants by Laplace Expansion and Inverses by Adjoint Matrices, Trinity College Dublin, Michaelmas 2016 (standard reference, not scraped)