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.

✓ 7 results · all verified · 0 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Determinants over a Ring: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

None yet.

5 · Examples, counterexamples and false statements

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The Leibniz formula gives $\det (\begin{array}{cc} a & b \\ c & d \end{array}) = a d - b c$

Example

For every commutative ring, $\det (\begin{array}{cc} a & b \\ c & d \end{array}) = a d - b c .$

Facts & Assumptions

Given: A $2 \times 2$ matrix $A = (\begin{array}{cc} a & b \\ c & d \end{array})$ over a commutative ring.

[L1]

Determinant is the signed Leibniz sum over $S_{2}$ (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[L2]

Sign is $(- 1)$ to the inversion number (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations).

Verification

technique · direct

1.1

The two permutations of $2 = {0, 1}$ are the identity, with sign $1$ , and the swap, with one inversion and sign $- 1$ .

L1L2

2.1

Their Leibniz monomials are $a_{00} a_{11} = a d$ and $a_{10} a_{01} = c b = b c$ , so the signed sum is $a d - b c$ .

step 1.1algebra∎

ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A full $3 \times 3$ Leibniz expansion lists all six permutations and their signs

Example

For $A = (a_{i j}) \in M_{3} (R)$ , $\det A = a_{00} a_{11} a_{22} + a_{10} a_{21} a_{02} + a_{20} a_{01} a_{12} - a_{10} a_{01} a_{22} - a_{20} a_{11} a_{02} - a_{00} a_{21} a_{12} .$

Facts & Assumptions

Given: A $3 \times 3$ matrix over a commutative ring.

[L1]

The determinant is the signed Leibniz sum (For $n \geq 1$ , the determinant over a commutative ring by the Leibniz formula, and $∣ \det A ∣$ for a real matrix).

[L2]

A permutation's sign is determined by the parity of its inversions (Inversions, inversion number, the sign $sgn (σ) = (- 1)^{inv (σ)}$ , and even and odd permutations).

[L3]

A set of size $3$ has $3! = 6$ bijections to itself (A finite set $A$ with $∣ A ∣ = n$ has exactly $n!$ bijections onto itself, and $n!$ bijections onto any set of the same cardinality).

Verification

technique · direct

1.1

The even permutations in one-line notation are $[0, 1, 2]$ , $[1, 2, 0]$ and $[2, 0, 1]$ ; the odd ones are $[1, 0, 2]$ , $[2, 1, 0]$ and $[0, 2, 1]$ . These are all six permutations.

L1L2L3

2.1

Substitution yields the displayed six terms. For $A = (\begin{array}{ccc} 1 & 2 & 3 \\ 0 & 1 & 4 \\ 5 & 6 & 0 \end{array})$ they give $0 + 0 + 40 - 0 - 15 - 24 = 1$ , a concrete check of the signs.

step 1.1algebra∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

An integer matrix of determinant $2$ is invertible over $Q$ but not over $Z$

Example

The integer matrix $A = diag (2, 1)$ has determinant $2$ . It is invertible as a matrix over $Q$ , but it is not invertible as a matrix over $Z$ .

Facts & Assumptions

Given: $A = (\begin{array}{cc} 2 & 0 \\ 0 & 1 \end{array})$ .

[L1]

The $2 \times 2$ determinant is $a d - b c$ (The Leibniz formula gives $\det (\begin{array}{cc} a & b \\ c & d \end{array}) = a d - b c$ ).

[L2]

An invertible matrix over a commutative ring has unit determinant (An invertible square matrix over a commutative ring has unit determinant).

[L3]

The rationals form a field (The rationals form a field).

[L4]

The integers form a commutative ring (The integers form a commutative ring).

[L5]

The only units of $Z$ are $1$ and $- 1$ ( $(Z, \cdot, 1)$ is a commutative monoid whose group of units is ${1, - 1}$ ; equivalently $u ∣ 1$ holds exactly for $u = 1$ and $u = - 1$ ).

Verification

technique · direct

1.1

Fact [L1] gives $\det A = 2$ . Over $Q$ , the matrix $diag (1 / 2, 1)$ multiplies with $A$ in either order to give $I_{2}$ , so $A$ is invertible there.

L1L2L3L4L5algebra

2.1

Over $Z$ , the determinant $2$ is not a unit by [L5]. The contrapositive of [L2] therefore rules out an integer inverse.

step 1.1L2L5∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

Over $Z / 2$ , an antisymmetric bilinear form need not be alternating

Statement refuted

The false converse is: every antisymmetric bilinear function is alternating. Over $R = Z / 2$ , define $F : M_{2} (R) \to R$ on columns $x, y \in R^{2}$ by $F ([x ∣ y]) = x_{0} y_{0}$ . Then $F$ is bilinear and antisymmetric but not alternating.

Facts & Assumptions

Given: The field $R = Z / 2$ and the displayed function $F$ .

[L1]

Antisymmetric means that swapping columns negates the value, while alternating means vanishing on equal columns (Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring).

[L2]

$Z / 2$ is a field (For every prime $p$ , the two operations on $Z / p$ make it a field).

[L3]

In $Z / 2$ , addition and multiplication are modulo $2$ , so $- 1 = 1$ (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

Counterexample

technique · direct

1.1

The coordinate product is linear in each column. Moreover $F ([y ∣ x]) = y_{0} x_{0} = x_{0} y_{0} = - F ([x ∣ y])$ because multiplication is commutative and $- 1 = 1$ in $R$ . Thus $F$ is antisymmetric.

L1L2L3algebra

2.1

For $e_{0} = (1, 0)^{T}$ , one has $F ([e_{0} ∣ e_{0}]) = 1$ , so $F$ does not vanish on equal columns and is not alternating.

step 1.1L1algebra∎

CounterexampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

The naive quaternionic formula $a d - b c$ is not row-alternating: a matrix with equal rows can have value $2 k \neq 0$

Statement refuted

The commutative-ring formula $a d - b c$ does not define a row-alternating determinant for quaternionic $2 \times 2$ matrices. A matrix with two equal rows can have naive value $2 k \neq 0$ .

Facts & Assumptions

Given: The quaternionic matrix $A = (\begin{array}{cc} i & j \\ i & j \end{array})$ and the naive expression $D (A) = a d - b c$ .

[L1]

The quaternions have basis elements $i, j, k$ and real scalar multiplication (The quaternions $H$ : real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$ ).

[L2]

Quaternion multiplication satisfies $i j = k$ , $j i = - k$ , and $k \neq - k$ ( $H$ is a division ring that is not commutative, hence not a field: $q^{- 1} = \overset{ˉ}{q} / N (q)$ for $q \neq 0$ , while $i j = k$ and $j i = - k$ ).

[L3]

Over a commutative ring the genuine $2 \times 2$ determinant formula is $a d - b c$ (The Leibniz formula gives $\det (\begin{array}{cc} a & b \\ c & d \end{array}) = a d - b c$ ).

Counterexample

technique · direct

1.1

The two rows of $A$ are both $(i, j)$ , so a row-alternating function would vanish on $A$ .

L1L2L3

2.1

The naive expression instead gives $D (A) = i j - j i = k - (- k) = 2 k$ . If $2 k = 0$ , then $k = - k$ , contrary to [L2]; hence $D (A) \neq 0$ .

step 1.1L2algebra∎

ExampleConstruction: AI-generatedVerification: AI-generatedprecheck passaudited 2026-08-11Open item page →

Row operations track determinant correctly for a singular triangular matrix over $Z / 6$

Example

Over $R = Z / 6$ , let $A = diag (2, 1)$ . Then $A$ is not invertible although $\det A = 2 \neq 0$ . A swap changes the determinant to $4 = - 2$ , scaling the first row by the nonzero nonunit $3$ changes it to $0 = 3 \cdot 2$ , and adding four times the second row to the first leaves it equal to $2$ .

Facts & Assumptions

Given: The displayed matrix over $Z / 6$ .

[L1]

Row swaps, arbitrary scalings and row additions have the three determinant laws without a nonsingularity assumption (For every square matrix, including singular ones, a row swap negates the determinant, scaling a row by any scalar scales it, and row addition leaves it unchanged).

[L2]

A triangular determinant is the product of its diagonal entries (The determinant of a triangular matrix is the product of its diagonal entries).

[L3]

Arithmetic in $Z / 6$ is commutative ring arithmetic modulo $6$ (For every natural $n$ , $(Z / n, +)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).

[L4]

$Z / 6$ consists of congruence classes modulo $6$ (The congruence class $[a]_{n}$ and the quotient set $Z / n$ ).

[L5]

An invertible matrix over a commutative ring has unit determinant (An invertible square matrix over a commutative ring has unit determinant).

Verification

technique · direct

1.1

By [L2], $\det A = 2$ . The element $2$ is not a unit modulo $6$ , since every product $2 r$ is even and cannot be congruent to $1$ ; therefore [L5] implies that $A$ is not invertible.

L1L2L3L4L5algebra

2.1

Swapping rows gives $(\begin{array}{cc} 0 & 1 \\ 2 & 0 \end{array})$ with determinant $- 2 = 4$ . Scaling row $0$ by $3$ gives $diag (0, 1)$ with determinant $0 = 3 \cdot 2$ . Replacing row $0$ by row $0 + 4 R_{1}$ gives $(\begin{array}{cc} 2 & 4 \\ 0 & 1 \end{array})$ with determinant $2$ .

step 1.1algebra

3.1

These values agree respectively with negation, multiplication by $3$ , and invariance under row addition in [L1]. No cancellation, unit scaling or invertibility was used.

step 2.1L1∎

False statementConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-11Open item page →

FALSE: $\det (A + B) = \det (A) + \det (B)$ for all same-sized square matrices

Statement

The following claim is false: for all same-sized square real matrices, $\det (A + B) = \det (A) + \det (B) .$

Facts & Assumptions

Given: Over $R$ , take $A = B = I_{2}$ .

[L1]

Matrix addition is entrywise and $I_{2}$ has diagonal entries $1$ (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

[L2]

Determinant is multilinear in one selected row or column while all other rows or columns are fixed (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

[L3]

For a $2 \times 2$ matrix, determinant is $a d - b c$ (The Leibniz formula gives $\det (\begin{array}{cc} a & b \\ c & d \end{array}) = a d - b c$ ).

[L4]

The real numbers form a field (The reals form a field).

Refutation

technique · direct

1.1

Here $A + B = 2 I_{2}$ , so [L3] gives $\det (A + B) = 4$ , whereas $\det (A) + \det (B) = 1 + 1 = 2$ . Since $4 \neq 2$ in $R$ , the claim fails.

L1L3L4algebra

2.1

The property in [L2] does not imply whole-matrix additivity: changing both rows at once produces cross terms. It permits addition only in one selected row or column while all the others remain fixed.

step 1.1L2∎

Determinants over a Ring: Examples and Counterexamples

1 · Prerequisites

2 · Summary

3 · Logical flowchart

4 · Definitions, theorems and proofs

5 · Examples, counterexamples and false statements

The Leibniz formula gives det⁡(abcd)=ad−bcdet(ac​bd​)=ad−bc

Example

Facts & Assumptions

Verification

A full 3×33×3 Leibniz expansion lists all six permutations and their signs

Example

Facts & Assumptions

Verification

An integer matrix of determinant 22 is invertible over QQ but not over ZZ

Example

Facts & Assumptions

Verification

Over Z/2Z/2, an antisymmetric bilinear form need not be alternating

Statement refuted

Facts & Assumptions

Counterexample

The naive quaternionic formula ad−bcad−bc is not row-alternating: a matrix with equal rows can have value 2k≠02k=0

Statement refuted

Facts & Assumptions

Counterexample

Row operations track determinant correctly for a singular triangular matrix over Z/6Z/6

Example

Facts & Assumptions

Verification

FALSE: det⁡(A+B)=det⁡(A)+det⁡(B)det(A+B)=det(A)+det(B) for all same-sized square matrices

Statement

Facts & Assumptions

Refutation

Sources

The Leibniz formula gives $\det (\begin{array}{cc} a & b \\ c & d \end{array}) = a d - b c$

A full $3 \times 3$ Leibniz expansion lists all six permutations and their signs

An integer matrix of determinant $2$ is invertible over $Q$ but not over $Z$

Over $Z / 2$ , an antisymmetric bilinear form need not be alternating

The naive quaternionic formula $a d - b c$ is not row-alternating: a matrix with equal rows can have value $2 k \neq 0$

Row operations track determinant correctly for a singular triangular matrix over $Z / 6$

FALSE: $\det (A + B) = \det (A) + \det (B)$ for all same-sized square matrices