Alphabeta MathHow 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, and The corresponding entrywise additive and scalar laws also hold, including all zero-sized shapes.
Facts & Assumptions
Given: A commutative ring and matrices of compatible finite shapes over .
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).
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).
Ring multiplication distributes over addition, annihilates zero and obeys the usual sign laws (In any ring , , , and ).
Proof
Entrywise ring addition gives its abelian-group laws. Substitution in the product formula gives and both distributive laws, since all off-diagonal identity terms are zero and the diagonal term is one.
For compatible , the entry of is , while that of is . Distributivity and finite-sum Fubini turn both into .
The entry of is , the entry of ; transposing twice restores each entry. Empty sums are zero, so every argument also covers zero-sized shapes.
Depends on
- Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose
- Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule
- In any ring $0 \cdot a = a \cdot 0 = 0$, $(-a)b = a(-b) = -(ab)$, $(-a)(-b) = ab$, $(-1)a = -a$ and $a(b - c) = ab - ac$
Used by
- An invertible square matrix over a commutative ring has unit determinant Corollary
- Over a field, for each right-hand side b, Ax=b has a unique solution exactly when det(A) is nonzero, and then Cramer's quotient formula holds Corollary
- Similar matrices over a commutative ring have the same determinant Corollary
- Invertible square matrices and similarity over a commutative ring Definition
- For n≥ 1, determinant is a natural transformation det:GLₙ(-)⟹(-)^× from commutative rings to groups Example
- For A∈ Mₙ(R) and columns u,v over a commutative ring, det(A+uv^T)=det(A)+v^Tadj(A)u Lemma
- For symmetric M=beginpmatrixA&BB^T&C endpmatrix with A invertible, a block-unitriangular congruence gives A⊕(C-B^TA⁻¹B) and factors det M Lemma
- Formally, (I-xA)⁻¹=∑_n≥0Aⁿ xⁿ over every commutative coefficient ring Lemma
- The companion matrix advances the recurrence state vector by one step Proposition
- Cramer's rule over a commutative ring: every solution satisfies det(A)xⱼ=det(Aⱼ(b)), and a unit determinant gives the unique quotient formula Theorem
- Every finite Galois extension of an infinite field has a normal basis Theorem
- Every nonzero commutative ring has invariant basis number for finite bases Theorem
- For A,B∈ Mₙ(F), the products AB and BA have the same characteristic polynomial Theorem
- For every positive-sized square matrix over a commutative ring, Aadj(A)=adj(A)A=det(A)I Theorem
- For same-sized finite square matrices over a commutative ring, det(AB)=det(A)det(B) Theorem
- Over a commutative ring, adj(P⁻¹AP)=P⁻¹adj(A)P for every invertible P Theorem
- The (u,v) entry of Aⁿ is the total weight of length-n walks from u to v Theorem
Dependency tree · two levels
15 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
- S. New, MATH 146 Linear Algebra 1 Lecture Notes, Ch. 4 (standard reference, not scraped)
- P. Massot, Structures algébriques fondamentales, §6.4 (standard reference, not scraped)