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.

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 (B C) = (A B) C, I_{m} A = A = A I_{n},$ $A (B + C) = A B + A C, (A + B) C = A C + B C,$ and $(A B)^{T} = B^{T} A^{T}, (A^{T})^{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).

[L3]

Ring multiplication distributes over addition, annihilates zero and obeys the usual sign laws (In any ring $0 \cdot a = a \cdot 0 = 0$ , $(- a) b = a (- b) = - (a b)$ , $(- a) (- b) = a b$ , $(- 1) a = - a$ and $a (b - c) = a b - a c$ ).

Proof

technique · direct

1.1L1L3algebra

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

2.1step 1.1L2L3algebra

For compatible $A, B, C$ , the $(i, ℓ)$ entry of $(A B) C$ is $\sum_{k} (\sum_{j} a_{i j} b_{j k}) c_{k ℓ}$ , while that of $A (B C)$ is $\sum_{j} a_{i j} (\sum_{k} b_{j k} c_{k ℓ})$ . Distributivity and finite-sum Fubini turn both into $\sum_{j, k} a_{i j} b_{j k} c_{k ℓ}$ .

3.1step 2.1L1L2algebra∎

The $(k, i)$ entry of $(A B)^{T}$ is $\sum_{j} a_{i j} b_{j k} = \sum_{j} b_{j k} a_{i j}$ , the $(k, i)$ entry of $B^{T} A^{T}$ ; transposing twice restores each entry. Empty sums are zero, so every argument also covers zero-sized shapes.

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

Statement

Facts & Assumptions

Proof

Depends on

Dependency tree · 2 levels

Sources