DefinitionDefinition: Literature-sourcedProof: Not applicableaudited 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.

Rectangular matrix multiplication and the identity matrix $I_{n}$ , including zero-sized shapes

Definition

Let $F$ be a field, let $m, n, p \in N$ , and let $A = (a_{i j}) \in M_{m \times n} (F)$ and $B = (b_{j k}) \in M_{n \times p} (F)$ . Their matrix product is the matrix $A B \in M_{m \times p} (F)$ whose entries are

$(A B)_{i k} : = \sum_{j \in n} a_{i j} b_{j k} .$

The sum is the finite sum in the additive commutative monoid of $F$ . If $n = 0$ , it is the empty sum, so $A B$ is the zero matrix of shape $m$ by $p$ .

The identity matrix $I_{n} \in M_{n} (F)$ has entry $1$ when $i = j$ and entry $0$ when $i \neq j$ . In particular, $I_{0}$ is the unique empty matrix in $M_{0} (F)$ .

Depends on

Used by

Exact-arithmetic LSQR with Golub–Kahan bidiagonalization and explicit statuses Algorithm
Finite recursive Galerkin V- and W-cycle for an SPD hierarchy Algorithm
Finite strength-graph aggregation and Galerkin hierarchy with explicit statuses Algorithm
Finite-budget inexact Newton–Krylov with a descent safeguard Algorithm
Finite-budget Levenberg-Marquardt with a trust-ratio safeguard Algorithm
Finite-memory capped DIIS projector proposal with fallback Algorithm
Flexible GMRES with variable right preconditioning Algorithm
General-RHS Hermitian Toeplitz solve by reflection recursion and Gohberg–Semencul Algorithm
Gram-matrix AdaGrad with full or singular diagonal metrics Algorithm
The rank of a matrix equals the rank of the linear map x↦ Ax Corollary
A first resolvent estimate does not ensure the prescribed semigroup bound Counterexample
A fully converged LSQR solve can amplify a small singular-direction error Counterexample
BCH truncation fails when higher commutators do not vanish Counterexample
Coercive non-symmetric forms need not have an orthonormal eigenbasis Counterexample
The product of ILU(0) factors can contain a fill position Counterexample
A finite family of subsets of [n] and its incidence matrix over F Definition
A normalised LU factorisation has a unit lower-triangular L and an upper-triangular U Definition
Bfgs curvature pairs and Hessian/inverse updates Definition
Block LU factorisation and the associated Schur complement Definition
Conservative nonnegative network advection routing Definition
Cuspidal representations and Harish-Chandra series Definition
Dirac Notation Conversion Definition
Discrete linear input-state-output experiments Definition
Elementary matrices obtained by applying one elementary row operation to an identity matrix Definition
Finite column generator Definition
Finite nonlinear observation designs, local identifiability, and weighted information Definition
Finite weighted network diffusion data Definition
Finite-basis projector energy model Definition
Finite-dimensional linear contextual bandit model Definition
Finite-dimensional Schwarz subspace-correction data Definition
Fixed-particle finite-temperature density-matrix free energy Definition
Forward and backward substitution for triangular linear systems Definition
Full-rank lattices, covolume, and the dual lattice Definition
Galerkin coarse matrices and the exact coarse-correction error map Definition
Generator and parity-check matrices over a finite field Definition
Invertible matrices and the general linear group GLₙ(F) Definition
Lower-shift displacement rank and generator pairs Definition
Matrix equation Ax=b, its solution set, consistency, homogeneous systems and the augmented matrix [A∣ b] Definition
Ordered partitions and coordinate parabolics Definition
Pauli measurement branch semantics Definition

…and 153 more results.

Dependency tree · two levels

13 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. Axler, Linear Algebra Done Right, 4th ed., §3C (standard reference, not scraped)

Rectangular matrix multiplication and the identity matrix InIn​, including zero-sized shapes