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.
The vector space of by matrices over a field, with entrywise operations
Definition
Let be a field (Field) and let . Recall that a natural number is a von Neumann natural (The natural numbers (von Neumann)), so and (On the order is membership: ), and let be their cartesian product. An by matrix over is an element of the function space (The vector space of all functions with pointwise operations, and as the case ), that is a function ; we write
for its entries, being the row index and the column index. Write
and for the square case.
Since is the function space , it is a vector space over with the pointwise operations of The vector space of all functions with pointwise operations, and as the case , which read entrywise:
and the zero of is the matrix all of whose entries are . No verification is needed beyond that already carried out in The vector space of all functions with pointwise operations, and as the case for an arbitrary index set: this is the case .
Both indices start at . The rows are indexed by and the columns by , so the entries of a by matrix are .
The degenerate shapes. contains , so and are genuine cases. If or then , so has exactly one element, the empty function, and is the zero space; there is no matrix of shape by other than that one.
Remarks
-
This item introduces the vector-space structure and the notation, and nothing else. There is no matrix product here, no identity matrix, no ring , no determinant and no matrix of a linear map. Those belong to a later page, which must add the product to this object rather than introduce a second notion of matrix; the addition and the scalar multiplication used there are the entrywise ones defined above.
-
A matrix is a function, so equality of matrices is equality of functions: exactly when for all and . Nothing below relies on a matrix being written as a rectangular array; the array is a way of displaying the function.
-
Why the shape is a pair of naturals rather than a pair of finite index sets. Taking the index set to be with and natural numbers keeps the coordinates of a matrix, of a tuple in (The vector space of all functions with pointwise operations, and as the case ) and the finite sums of The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity all indexed by the same kind of object, which is what makes the boundary cases above statable at all.
Depends on
Used by
- Exact-arithmetic LSQR with Golub–Kahan bidiagonalization and explicit statuses Algorithm
- Flexible GMRES with variable right preconditioning Algorithm
- Mₙ(F) is a ring under entrywise addition and matrix multiplication, including the zero ring M₀(F) Corollary
- A fully converged LSQR solve can amplify a small singular-direction error Counterexample
- A finite family of subsets of [n] and its incidence matrix over F Definition
- Compressed sparse row matrices with stored-entry semantics Definition
- Conservative nonnegative network advection routing Definition
- Coordinate columns [v]_B and matrices [T]_B^C of linear maps relative to ordered bases Definition
- Discrete linear input-state-output experiments Definition
- Elementary row operations and row equivalence for finite matrices over a field Definition
- Finite column generator Definition
- Finite weighted network diffusion data Definition
- Generator and parity-check matrices over a finite field Definition
- Matrix equation Ax=b, its solution set, consistency, homogeneous systems and the augmented matrix [A∣ b] Definition
- Matrix units Eᵢⱼ and the Kronecker delta Definition
- Pauli measurement branch semantics Definition
- Quantum acceptance probability for a finite promise computation Definition
- Rectangular matrix multiplication and the identity matrix Iₙ, including zero-sized shapes Definition
- Row echelon form, reduced row echelon form, leading entries, pivots, pivot positions and pivot columns Definition
- Row space, column space, nullspace, row rank, column rank and matrix rank Definition
- Structural graphs and ordered symmetric elimination Definition
- Symmetric saddle-point system, Schur complement, and block preconditioners Definition
- The Euclidean logarithmic norm of a complex matrix Definition
- The Gram matrix G(v₀,…,vᵣ₋₁)=(⟨ vᵢ,vⱼ⟩)_i,j<r and Gram determinant, with empty value 1 Definition
- The Hessian matrix and critical points of a scalar field Definition
- The inclusion matrix W_t,k(n) of t-sets against k-sets Definition
- The phi-function family by everywhere-convergent series Definition
- The strict nullspace property Definition
- The trace tr(A) as the sum of the diagonal entries Definition
- The transpose A^T of a matrix Definition
- A short Reed–Solomon code over F₅ and its symbol-error syndromes Example
- For a field extension K/F, one has K⊗_FMₙ(F)≅ Mₙ(K) as K-algebras Example
- Matrix-unit rotation for a k–Mₙ(k) Morita pair Example
- The binary [7,4,3] Hamming code and its single-error syndromes Example
- The Frobenius inner product on a real or complex matrix space Example
- Finite matrix and module preliminaries: right inverses, rank invariance, finite length and nilpotent trace Lemma
- Finite matrix exponential series and its identities Lemma
- Gaussian integral for a positive-definite quadratic form Lemma
- Pauli measurement projectors and total probability Lemma
- The conditional Gaussian mixture is a nonnegative supermartingale Lemma
…and 13 more results.
Dependency tree · two levels
25 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
- Matrix (mathematics) (Wikipedia) (standard reference, not scraped)
- Examples of vector spaces (Wikipedia) (standard reference, not scraped)