Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-03
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: dimFV=nullityT+rankT\dim_F V=\operatorname{nullity}T+\operatorname{rank}T

Statement

Let T:VWT:V\to W be a linear map of vector spaces over FF, with VV finite-dimensional. Then

dimFV=nullityT+rankT.\dim_F V=\operatorname{nullity}T+\operatorname{rank}T.

Equivalently,

dimFV=dimF(kerT)+dimF(imT).\dim_F V=\dim_F(\ker T)+\dim_F(\operatorname{im}T).

Facts & Assumptions

Given: A linear map T:VWT:V\to W with VV finite-dimensional over FF.

[L1]

Nullity and rank are the dimensions of the kernel and image (Rank and nullity of a linear map with finite-dimensional domain).

[L2]

There are finite bases KK of kerT\ker T and BB of VV with KBK\subseteq B; for C=BKC=B\setminus K, the set CC is finite, T[C]T[C] is a basis of imT\operatorname{im}T, and TC:CT[C]T|_C:C\to T[C] is bijective (Extending a basis of the kernel to a basis of the domain gives a basis of the image).

[L3]

The dimension of a finite-dimensional vector space is the number of elements in any finite basis (Finite-dimensional vector space, and its dimension dimFV\dim_F V; infinite-dimensional means having no finite basis).

[L5]

A bijection between finite sets transports their cardinality (The cardinality A\lvert A\rvert of a finite set, consequence (c)).

Proof

technique · direct
1.1

Choose K,B,CK,B,C as in [L2]. Since B=K˙CB=K\mathbin{\dot\cup}C, [L4] gives B=K+C|B|=|K|+|C|. The bijection TC:CT[C]T|_C:C\to T[C] gives C=T[C]|C|=|T[C]|.

L2L4L5given
2.1

Since BB, KK, and T[C]T[C] are bases of VV, kerT\ker T, and imT\operatorname{im}T, respectively, [L1] and [L3] turn step 1.1 into dimFV=nullityT+rankT\dim_F V=\operatorname{nullity}T+\operatorname{rank}T.

step 1.1L1L2L3
3.1

The displayed equivalent form follows by unfolding the definitions of rank and nullity.

step 2.1L1

Remarks

Depends on

Used by

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