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.
Finite rectangular matrices over a commutative ring, their entries, rows and columns
Definition
Let be a commutative ring and let . An matrix over is a function Its value at is written . The set of all such matrices is , and .
For , row is the function on ; for , column is the function on . This includes zero-sized shapes: a matrix with empty index set is the unique function from that empty set.
Depends on
Used by
- Column-multilinear, alternating, normalized and antisymmetric functions on square matrices over a commutative ring Definition
- Entrywise ring-matrix operations, rectangular matrix products, identity matrices and transpose Definition
- For n≥1, the determinant over a commutative ring by the Leibniz formula, and |det A| for a real matrix Definition
- Row swaps, arbitrary row scalings and row additions over a commutative ring, with reversible elementary cases distinguished Definition
- Upper triangular, lower triangular and diagonal square matrices over a commutative ring Definition
- For n≥ 1, determinant is a natural transformation det:GLₙ(-)⟹(-)^× from commutative rings to groups Example
- For a field, the ring-matrix operations, invertibility and similarity agree exactly with the established field-matrix interface Proposition
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 31 results over 17 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- S. New, MATH 146 Linear Algebra 1 Lecture Notes, Notation 4.16 (standard reference, not scraped)