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.
Rank-nullity:
Statement
Let be a linear map of vector spaces over , with finite-dimensional. Then
Equivalently,
Facts & Assumptions
Given: A linear map with finite-dimensional over .
Nullity and rank are the dimensions of the kernel and image (Rank and nullity of a linear map with finite-dimensional domain).
There are finite bases of and of with ; for , the set is finite, is a basis of , and is bijective (Extending a basis of the kernel to a basis of the domain gives a basis of the image).
The dimension of a finite-dimensional vector space is the number of elements in any finite basis (Finite-dimensional vector space, and its dimension ; infinite-dimensional means having no finite basis).
If two finite sets are disjoint, the cardinality of their union is the sum of their cardinalities (The sum rule: a finite disjoint union is finite with and , and a sum over a finite index set splits along a partition, clause 1).
A bijection between finite sets transports their cardinality (The cardinality of a finite set, consequence (c)).
Proof
Choose as in [L2]. Since , [L4] gives . The bijection gives .
Since , , and are bases of , , and , respectively, [L1] and [L3] turn step 1.1 into .
The displayed equivalent form follows by unfolding the definitions of rank and nullity.
Remarks
- If , all three dimensions are zero and the formula reads ; no positive-dimension hypothesis is hidden.
- No finite-dimensionality assumption is made on . The image is finite-dimensional for the reason isolated in Extending a basis of the kernel to a basis of the domain gives a basis of the image.
Depends on
- Rank and nullity of a linear map with finite-dimensional domain
- Extending a basis of the kernel to a basis of the domain gives a basis of the image
- Finite-dimensional vector space, and its dimension $\dim_F V$; infinite-dimensional means having no finite basis
- The cardinality $\lvert A\rvert$ of a finite set
- The sum rule: a finite disjoint union is finite with $\lvert A \cup B\rvert = \lvert A\rvert + \lvert B\rvert$ and $\lvert\bigcup_{i \in I} A_i\rvert = \sum_{i \in I}\lvert A_i\rvert$, and a sum over a finite index set splits along a partition
Used by
- For an m× n matrix A, rank(A)+dim N(A)=n Corollary
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 100 results over 24 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
- UCLA Algebra Notes, rank-nullity theorem (standard reference, not scraped)
- Axler, Linear Algebra Done Right, 4th ed., Chapter 3 (standard reference, not scraped)