Alphabeta Math
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.

✓ 17 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 17 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

Determinants of Matrices over a Commutative Ring

1 · Prerequisites

2 · Summary

Commutative rings provide finite sums, products and units, while the earlier matrix interface supplies field-valued multiplication, transpose, invertibility and similarity. Finite permutations and their sign homomorphism license the Leibniz formula, and finite counting makes its index set explicit. Gaussian elimination supplies the real row-reduction criterion used at the field boundary, while the established finite multivariate-polynomial construction licenses the determinant polynomial in the matrix entries.

Ring-valued matrix arithmetic is developed first and reconciled with the field interface. Alternating multilinear functions then yield the Leibniz determinant and its uniqueness, followed by vanishing, transpose and row-operation laws. Triangular determinants and rigidity prove multiplicativity without assuming invertibility. Unit determinants, inverses and similarity follow over a commutative ring; specialization to real matrices proves that nonzero determinant is equivalent to invertibility, and the explicit Leibniz sum exhibits determinant as a polynomial in the entries.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Finite rectangular matrices over a commutative ring, their entries, rows and columns

Definition

Let R be a commutative ring and let m,n∈N. An m×n matrix over R is a function A:m×n⟶R. Its value at (i,j) is written aij. The set of all such matrices is Mm×n(R), and Mn(R):=Mn×n(R).

For i<m, row i is the function j↦aij on n; for j<n, column j is the function i↦aij on m. This includes zero-sized shapes: a matrix with empty index set is the unique function from that empty set.

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose

Definition

Let R be a commutative ring. Matrices of one shape are added and scaled entrywise. For A∈Mm×n(R) and B∈Mn×p(R), their product is AB∈Mm×p(R) with (AB)ik:=∑j<naijbjk. The sum is the finite sum in the additive commutative monoid of R, and is 0 when n=0.

The identity matrix In has entry 1 on the diagonal and 0 elsewhere. The transpose AT∈Mn×m(R) is defined by (AT)ji:=aij. The zero matrix has every entry 0.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products

Statement

For matrices over a commutative ring, whenever the shapes are compatible, A(BC)=(AB)C,ImA=A=AIn, A(B+C)=AB+AC,(A+B)C=AC+BC, and (AB)T=BTAT,(AT)T=A. The corresponding entrywise additive and scalar laws also hold, including all zero-sized shapes.

Facts & Assumptions

Given: A commutative ring R and matrices of compatible finite shapes over R.

[L1]

Matrix addition, multiplication, identity and transpose are given by their entrywise finite-sum formulas (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

[L2]

Finite sums in a commutative monoid may be reindexed and finite double sums may be taken in either order (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Proof

technique · direct
1.1

Entrywise ring addition gives its abelian-group laws. Substitution in the product formula gives ImA=A=AIn and both distributive laws, since all off-diagonal identity terms are zero and the diagonal term is one.

L1L3algebra
2.1

For compatible A,B,C, the (i,ℓ) entry of (AB)C is ∑k(∑jaijbjk)ckℓ, while that of A(BC) is ∑jaij(∑kbjkckℓ). Distributivity and finite-sum Fubini turn both into ∑j,kaijbjkckℓ.

step 1.1L2L3algebra
3.1

The (k,i) entry of (AB)T is ∑jaijbjk=∑jbjkaij, the (k,i) entry of BTAT; transposing twice restores each entry. Empty sums are zero, so every argument also covers zero-sized shapes.

step 2.1L1L2algebra∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Invertible square matrices and similarity over a commutative ring

Definition

Let R be a commutative ring. A matrix A∈Mn(R) is invertible when there is B∈Mn(R) with AB=In=BA. The inverse is unique and is denoted A−1. The general linear group over R is GL⁡n(R):={A∈Mn(R):A is invertible}.

Matrices A,B∈Mn(R) are similar over R when there is P∈GL⁡n(R) such that B=P−1AP. Associativity and the identity laws from Matrix arithmetic over a commutative ring is associative, unital and distributive, and transpose reverses products make these the usual units and conjugacy relation in the matrix monoid.

PropositionStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-11Open item page →

For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface

Statement

Let F be a field. Viewing F as a commutative ring, the ring-valued matrix set, addition, multiplication, identity, transpose, invertibility, inverse and similarity defined here are exactly the corresponding established field-matrix notions.

Facts & Assumptions

Given: A field F regarded as a commutative ring.

[L1]

A ring-valued m×n matrix is a function m×n→F (Finite rectangular matrices over a commutative ring, their entries, rows and columns).

[L2]

Ring-matrix operations, products, identities and transpose use the entrywise finite-sum formulas (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

[L4]
[L5]

Field-matrix transpose interchanges the same entries (The transpose AT of a matrix).

[L6]

Every field is a commutative ring with the same operations and identities (Every field is a commutative ring with 1≠0; it is an integral domain, and it is a commutative division ring).

[L7]

Ring-matrix invertibility and similarity are defined by AB=BA=I and B=P−1AP (Invertible square matrices and similarity over a commutative ring).

[L8]

Field-matrix invertibility uses the same two-sided inverse equations (Invertible matrices and the general linear group GL⁡n(F)).

[L9]

Field-matrix similarity uses the same conjugation equation (Similar matrices: B=P−1AP for an invertible P).

Proof

technique · direct
1.1

By [L1], [L3] and [L6], both matrix carriers are the same function set. The formulas in [L2], [L4] and [L5] agree entry for entry, including empty sums and zero-sized shapes.

L1L2L3L4L5L6
2.1

Since the products and identities agree, the two-sided inverse equations in [L7] and [L8] select the same matrices and the same unique inverses; then the conjugation formulas in [L7] and [L9] select the same similar pairs.

step 1.1L7L8L9∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring

Definition

Fix n≥1 and a commutative ring R. A function F:Mn(R)→R is column-multilinear when, with all other columns fixed, it is additive and compatible with scalar multiplication in each selected column.

It is alternating when F(A)=0 whenever two columns of A are equal. It is antisymmetric when interchanging two columns negates its value. It is normalized when F(In)=1. These conditions are stated over the ring itself and do not assume that 2 is invertible.

LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every alternating multilinear matrix function is antisymmetric under a column swap

Statement

Let n≥1 and let F:Mn(R)→R be column-multilinear and alternating. Interchanging any two columns of A negates F(A). This holds over every commutative ring, including characteristic 2.

Facts & Assumptions

Given: An alternating column-multilinear function F and two selected column positions containing u and v.

[L1]

Alternation makes F vanish on equal columns, while multilinearity expands sums separately in each column (Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring).

Proof

technique · direct
1.1

Put u+v in both selected positions. Alternation gives 0=F(…,u+v,…,u+v,…).

L1
2.1

Expanding twice gives 0=F(…,u,…,v,…)+F(…,v,…,u,…) because the two equal-column terms vanish. Adding the inverse of the first term yields the antisymmetry formula, without dividing by 2.

step 1.1L1L2algebra∎
LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Every alternating multilinear F satisfies F(A)=F(I)∑σ∈Snsgn⁡(σ)∏iaσ(i),i

Statement

Let n≥1, let R be a commutative ring, and let F:Mn(R)→R be alternating and column-multilinear. Then for A=(ari), F(A)=F(In)∑σ∈Snsgn⁡(σ)∏i<naσ(i),i.

Facts & Assumptions

Given: A matrix A=(ari)∈Mn(R) and an alternating column-multilinear function F:Mn(R)→R.

[L2]

Alternating multilinear functions are antisymmetric under swaps (Every alternating multilinear matrix function is antisymmetric under a column swap).

[L7]

Every transposition factorisation of a permutation has parity prescribed by its inversion sign (Every transposition factorisation of σ has parity (−1)inv⁡(σ)).

Proof

technique · direct
1.1

For r<n, let er be the column with entry 1 in row r and 0 elsewhere. Since column i is ∑r<narier, repeated multilinearity expands F(A) as the finite sum over tuples (ri)i<n of (∏i<narii)F(er0,…,ern−1).

L1L5algebra
2.1

If a tuple repeats a row index, its F-value is zero by alternation. The surviving tuples use every element of n once, so they are precisely the permutations ri=σ(i).

step 1.1L1
3.1

Factor σ into transpositions. Repeated antisymmetry changes F(In) by one minus sign per transposition. Each transposition has sign −1, so [L4] identifies the product of these signs with sgn⁡(σ); equivalently [L3] and [L7] identify it with the factorisation-independent inversion parity. Substitution into step 2.1 gives the formula.

step 2.1L2L3L4L6L7algebra∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

For n≥1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣ for a real matrix

Definition

Let R be a commutative ring, let n≥1, and let A=(aij)∈Mn(R). Its determinant is det⁡(A):=∑σ∈Snsgn⁡(σ)∏i<naσ(i),i. The sum is finite because Sn has n! elements. The product is taken in R, so the signs 1 and −1 act through the ring identities. The formula uses columns indexed by i<n and rows indexed by σ(i).

When A is real, ∣det⁡A∣ means the ordinary real absolute value of its real determinant. It is not alternate notation for the determinant itself.

CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

For every fixed finite size at least one, the determinant of a real square matrix is a polynomial in its matrix entries

Statement

For each fixed n≥1, the function det⁡:Mn(R)→R is evaluation of the polynomial Pn:=∑σ∈Snsgn⁡(σ)∏i<nxσ(i),i in the n2 commuting variables xri.

Facts & Assumptions

Given: A fixed natural n≥1 and commuting indeterminates xri for r,i<n.

[L1]

The determinant is the finite Leibniz sum ∑σsgn⁡(σ)∏iaσ(i),i (For n≥1, the determinant over a commutative ring by the Leibniz formula, and ∣det⁡A∣ for a real matrix).

[L2]

Iteration constructs a polynomial ring in any finite list of commuting indeterminates over a commutative ring (Polynomial rings in finitely many commuting indeterminates by iteration).

[L3]

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

[L5]

Evaluation at a ring element is a unital ring homomorphism, so it respects finite sums and products (Universal property of R[x]: a coefficient homomorphism and the image of x determine a unique ring homomorphism).

Proof

technique · direct
1.1

By [L2]–[L4], the displayed finite sum of signed monomials is an element Pn of the real polynomial ring in the n2 variables xri.

L2L3L4
2.1

Iterate [L5] through the finite list of variables, sending each xri to ari. The resulting homomorphism sends each monomial to ∏i<naσ(i),i and therefore sends Pn to the Leibniz sum det⁡(A) from [L1].

step 1.1L1L2L5algebra
3.1

Hence determinant is the polynomial function given by this explicit finite sum of finite products in the matrix entries.

step 2.1∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring

Statement

For n≥1 and every commutative ring R, the Leibniz determinant det⁡:Mn(R)→R is column-multilinear, alternating and normalized.

Facts & Assumptions

Given: The Leibniz determinant of an n×n matrix over a commutative ring.

[L2]

Multilinear, alternating and normalized have the stated columnwise meanings (Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring).

[L5]

Composing a permutation on either side with a transposition reverses its inversion sign (Composing with a transposition reverses (−1)inv⁡(σ)).

Proof

technique · direct
1.1

With every column but column q fixed, each Leibniz monomial contains exactly one entry from column q. Distributing finite sums therefore proves additivity and scalar compatibility in that column, and q was arbitrary.

L1L2L4algebra
2.1

Suppose columns p,q are equal. Pair each σ with σ∘(p q). Commutativity makes the paired monomials equal, while [L5] makes their signs opposite, so every pair sums to zero and the determinant vanishes.

step 1.1L3L4L5algebra
3.1

At In, every nonidentity permutation selects an off-diagonal zero, while the identity term is 1. Thus det⁡(In)=1. This also covers n=1 and the zero ring, where the equality reads 0=0.

step 2.1L1L2algebra∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The determinant is the unique normalized alternating multilinear function on the columns

Statement

For n≥1 over a commutative ring, determinant is the unique function F:Mn(R)→R that is column-multilinear, alternating and normalized.

Facts & Assumptions

Given: A normalized alternating column-multilinear function F:Mn(R)→R.

[L1]

Every alternating column-multilinear function satisfies the rigidity formula F(A)=F(In)det⁡(A) (Every alternating multilinear F satisfies F(A)=F(I)∑σ∈Snsgn⁡(σ)∏iaσ(i),i).

[L2]

The Leibniz determinant itself is alternating, column-multilinear and normalized (The Leibniz determinant is column-multilinear, alternating and normalized over every commutative ring).

Proof

technique · direct
1.1

Fact [L2] proves existence of a function with the three properties.

L1L2
2.1

If F has them, normalization gives F(In)=1, so [L1] gives F(A)=det⁡(A) for every A. Hence the function is unique.

step 1.1L1algebra∎
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A square matrix with a zero column or two equal columns has determinant zero

Statement

Let n≥1. If a matrix in Mn(R) over a commutative ring has a zero column or has two equal columns, then its determinant is zero.

Facts & Assumptions

Given: A square matrix A over a commutative ring.

Proof

technique · direct
1.1

If one column is zero, multilinearity gives det⁡(A)=det⁡(A)+det⁡(A) by writing that column as 0+0; cancellation in the additive group gives det⁡(A)=0.

L1algebra
2.1

If two columns are equal, alternation in [L1] gives det⁡(A)=0 directly, regardless of whether the columns are adjacent.

step 1.1L1∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

For every square matrix over a commutative ring, det⁡(AT)=det⁡(A)

Statement

For every n≥1, every commutative ring R, and every A∈Mn(R), det⁡(AT)=det⁡(A).

Facts & Assumptions

Given: A square matrix A=(aij) over a commutative ring.

[L3]

Sign is a homomorphism into {1,−1}, so sgn⁡(σ−1)=sgn⁡(σ) (The sign is a homomorphism Sn→{+1,−1}, surjective exactly when n≥2).

Proof

technique · direct
1.1

Substituting [L2] into [L1] gives det⁡(AT)=∑σ∈Snsgn⁡(σ)∏i<nai,σ(i).

L1L2
2.1

Reindex the sum by τ=σ−1 and the product by j=σ(i). Commutativity and [L3] turn the expression into ∑τ∈Snsgn⁡(τ)∏j<naτ(j),j=det⁡(A).

step 1.1L3L4algebra∎
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The determinant is alternating and multilinear in the rows as well as in the columns

Statement

For n≥1, determinant on Mn(R) over a commutative ring is multilinear and alternating in the rows. Interchanging two rows negates the determinant.

Facts & Assumptions

Given: A square matrix whose selected row is varied, or whose two selected rows are interchanged.

[L3]

Transpose is defined by (AT)ji=aij, so it interchanges rows and columns (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

Proof

technique · direct
1.1

Transposition sends a selected row, a row sum, a row scaling or a row swap to the corresponding operation on a selected column, without changing determinant.

L1L3
2.1

Apply the column multilinearity and alternation of [L2] to the transpose, then apply [L1] again. The resulting identities are exactly row multilinearity and row alternation for the original matrix.

step 1.1L1L2∎
DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-11Open item page →

Row swaps, arbitrary row scalings and row additions over a commutative ring, with reversible elementary cases distinguished

Definition

For a matrix over a commutative ring R, a row transformation is one of: interchanging two rows; multiplying one row by any scalar c∈R; or adding c times one row to a distinct row.

A swap is reversible, as is row addition with reverse coefficient −c. A row scaling is reversible exactly when its scalar is a unit. These reversible transformations are the ring-level elementary row equivalences. When R is a field, they are exactly the elementary row operations of Elementary row operations and row equivalence for finite matrices over a field, since every nonzero scalar is a unit. A scaling by a nonunit, including possibly 0, is still a row transformation but is not called a row equivalence.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

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

Statement

Let n≥1 and let A∈Mn(R) be a matrix over a commutative ring.

  1. Interchanging two rows changes det⁡(A) to −det⁡(A).
  2. Multiplying one row by any c∈R changes it to cdet⁡(A).
  3. Adding c times one row to a distinct row leaves it equal to det⁡(A).

No invertibility assumption is made on A or on c.

Facts & Assumptions

Given: A square matrix A over a commutative ring and a row transformation.

[L1]

Determinant is alternating and multilinear in its rows (The determinant is alternating and multilinear in the rows as well as in the columns).

[L2]

Ring row transformations include swaps, scaling by any scalar, and addition of a multiple of a distinct row (Row swaps, arbitrary row scalings and row additions over a commutative ring, with reversible elementary cases distinguished).

Proof

technique · direct
1.1

Row multilinearity gives det⁡(…,cRp,…)=cdet⁡(A) for every scalar c, including c=0 and zero divisors.

L1L2L3
2.1

Row antisymmetry gives det⁡(A′)=−det⁡(A) when A′ is obtained by a row swap.

step 1.1L1L2
3.1

Replacing Rp by Rp+cRq expands the new determinant as det⁡(A)+cD, where D has row Rq in both positions p and q; alternation gives D=0, so the determinant is unchanged.

step 2.1L1L2algebra
4.1

The derivations used only row multilinearity and alternation, not cancellation, matrix invertibility or scalar invertibility. Hence all three formulas include singular matrices and arbitrary scalars.

step 3.1∎
DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 2026-08-11Open item page →

Upper triangular, lower triangular and diagonal square matrices over a commutative ring

Definition

Let R be a commutative ring, let n≥1, and let A=(aij)∈Mn(R). It is upper triangular when aij=0 for i>j, lower triangular when aij=0 for i<j, and diagonal when aij=0 whenever i≠j.

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

The determinant of a triangular matrix is the product of its diagonal entries

Statement

If A=(aij)∈Mn(R) is upper or lower triangular over a commutative ring, with n≥1, then det⁡(A)=∏i<naii.

Facts & Assumptions

Given: A triangular n×n matrix A over a commutative ring.

[L1]

Upper triangular means aij=0 for i>j, while lower triangular means aij=0 for i<j (Upper triangular, lower triangular and diagonal square matrices over a commutative ring).

[L2]

Proof

technique · direct
1.1

For an upper triangular matrix, a nonzero Leibniz term requires σ(i)≤i for every i. A permutation with these inequalities is the identity: starting at i=0 and proceeding upward, bijectivity forces σ(i)=i. Thus every nonidentity term contains a zero entry.

L1L2L3
2.1

The identity term has sign 1 and equals ∏i<naii, so it is the whole determinant.

step 1.1L2L3
3.1

For a lower triangular matrix the same argument uses σ(i)≥i and proceeds downward, again forcing the identity. The argument includes n=1 and makes no cancellation assumption, so zero divisors and the zero ring cause no exception.

step 2.1L1L2∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

For same-sized finite square matrices over a commutative ring, det⁡(AB)=det⁡(A)det⁡(B)

Statement

For n≥1 and A,B∈Mn(R) over a commutative ring, det⁡(AB)=det⁡(A)det⁡(B).

Facts & Assumptions

Given: A fixed matrix A∈Mn(R) and a variable matrix B∈Mn(R).

[L1]

Determinant is the unique normalized alternating column-multilinear matrix function (The determinant is the unique normalized alternating multilinear function on the columns).

[L2]

Every alternating column-multilinear F satisfies F(B)=F(In)det⁡(B) (Every alternating multilinear F satisfies F(A)=F(I)∑σ∈Snsgn⁡(σ)∏iaσ(i),i).

Proof

technique · direct
1.1

Define F(B):=det⁡(AB). Each column of AB is A times the corresponding column of B, so distributivity makes F column-multilinear; equal columns of B give equal columns of AB, so F is alternating.

L1L2L3L4
2.1

Since AIn=A, one has F(In)=det⁡(A).

step 1.1L3L4
3.1

Apply [L2] to F: det⁡(AB)=F(B)=F(In)det⁡(B)=det⁡(A)det⁡(B). Neither matrix was assumed invertible.

step 2.1L2algebra∎
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

An invertible square matrix over a commutative ring has unit determinant

Statement

Let n≥1. If A∈Mn(R) is invertible over a commutative ring, then det⁡(A) is a unit of R. More precisely, det⁡(A−1) is its inverse.

Facts & Assumptions

Given: An invertible matrix A with inverse A−1.

[L1]

Determinants multiply: det⁡(XY)=det⁡(X)det⁡(Y) (For same-sized finite square matrices over a commutative ring, det⁡(AB)=det⁡(A)det⁡(B)).

[L4]

Matrix invertibility gives AA−1=In=A−1A (Invertible square matrices and similarity over a commutative ring).

Proof

technique · direct
1.1

Apply [L1] to the two equations in [L4]: det⁡(A)det⁡(A−1)=det⁡(In)=1 and det⁡(A−1)det⁡(A)=1.

L1L3L4L5
2.1

Thus det⁡(A) is a unit with inverse det⁡(A−1) by [L2]. In the zero ring, 0=1 and the same two-sided equation still gives the unit conclusion.

step 1.1L2∎
TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

A finite square real matrix is invertible if and only if its determinant is nonzero

Statement

For every n≥1 and every real matrix A∈Mn(R), A is invertible⟺det⁡(A)≠0.

Facts & Assumptions

Given: A real square matrix A of positive finite size.

[L2]

An n×n RREF with fewer than n pivots has a zero row; its pivot columns increase from left to right (Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns).

[L3]

A square matrix is invertible exactly when its RREF is the identity, equivalently when it has n pivots (Invertible matrix theorem: invertibility, full pivot rank, RREF I, trivial nullspace and unique solvability are equivalent).

[L4]

A row swap negates determinant, nonzero real row scaling multiplies it by a nonzero scalar, and row addition leaves it unchanged (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).

[L5]

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

[L6]

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

[L7]

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

Proof

technique · direct
1.1

If A is invertible, [L1] and [L6] make det⁡(A) a unit of R, hence nonzero by [L7].

L1L6L7
1.2

Conversely suppose A is not invertible and row reduce it to its RREF R. By [L3], R has fewer than n pivots and hence a zero row. Its pivot in row i, when present, lies in a column at least i, so every entry below the diagonal is zero; thus R is upper triangular.

L1L2L3
2.1

The zero row forces a zero diagonal entry, so [L5] gives det⁡(R)=0.

step 1.2L5algebra
3.1

Along the finite real row reduction, swaps and row additions preserve whether determinant is zero, and a scaling uses a nonzero scalar whose inverse gives the reverse implication. Hence det⁡(A)=0.

step 2.1L4L7algebra
4.1

Steps 1.2–3.1 prove the contrapositive det⁡(A)≠0⇒A invertible; combining it with step 1.1 proves the equivalence.

step 1.1step 3.1∎
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

If A is invertible over a commutative ring, then det⁡(A−1)=det⁡(A)−1

Statement

Let n≥1. If A∈Mn(R) is invertible over a commutative ring, then det⁡(A−1)=det⁡(A)−1.

Facts & Assumptions

Proof

technique · direct
1.1

By [L2], [L4] and [L5], det⁡(A)det⁡(A−1)=det⁡(In)=1, so det⁡(A−1) is an inverse of the unit det⁡(A).

L1L2L3L4L5
2.1

Uniqueness of the inverse in [L3] gives det⁡(A−1)=det⁡(A)−1.

step 1.1L3∎
CorollaryStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11Open item page →

Similar matrices over a commutative ring have the same determinant

Statement

Let n≥1. If A,B∈Mn(R) are similar over a commutative ring, then det⁡(B)=det⁡(A).

Facts & Assumptions

Given: An invertible P with B=P−1AP.

[L1]

Similarity over R means B=P−1AP for an invertible P (Invertible square matrices and similarity over a commutative ring).

Proof

technique · direct
1.1

By [L1], [L2] and associativity, det⁡(B)=det⁡(P−1)det⁡(A)det⁡(P).

L1L2L3L4
2.1

Substitute [L3] and commute the scalar factors in R: det⁡(P)−1det⁡(P)=1, leaving det⁡(B)=det⁡(A).

step 1.1L3algebra∎

5 · Examples, counterexamples and false statements

None yet.

Sources