TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passaudited 2026-08-11

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.

For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$

Statement

For every $n \geq 1$ , every commutative ring $R$ , and every $A \in M_{n} (R)$ , $\det (A^{T}) = \det (A) .$

Facts & Assumptions

Given: A square matrix $A = (a_{i j})$ over a commutative ring.

[L1]

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

[L2]

Transpose satisfies $(A^{T})_{i j} = a_{j i}$ (Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose).

[L3]

Sign is a homomorphism into ${1, - 1}$ , so $sgn (σ^{- 1}) = sgn (σ)$ (The sign is a homomorphism $S_{n} \to {+ 1, - 1}$ , surjective exactly when $n \geq 2$ ).

[L4]

A finite sum may be reindexed by a bijection (Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule).

Proof

technique · direct

1.1L1L2

Substituting [L2] into [L1] gives $\det (A^{T}) = \sum_{σ \in S_{n}} sgn (σ) \prod_{i < n} a_{i, σ (i)}$ .

2.1step 1.1L3L4algebra∎

Reindex the sum by $τ = σ^{- 1}$ and the product by $j = σ (i)$ . Commutativity and [L3] turn the expression into $\sum_{τ \in S_{n}} sgn (τ) \prod_{j < n} a_{τ (j), j} = \det (A)$ .

For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources

For every square matrix over a commutative ring, $\det (A^{T}) = \det (A)$