Existing in Mathlib · Linear algebra
Rank–Nullity Theorem
A linear map collapses the directions in its kernel and carries the surviving quotient directions into its range. Those two cardinal-rank contributions recover the rank of the original domain.
- linear map
- kernel
- range
- quotient module
- cardinal rank
Exact theorem
Exact Mathlib statement
theorem LinearMap.rank_range_add_rank_ker {R M M₁ : Type*} [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁] [HasRankNullity R] (f : M →ₗ[R] M₁) : Module.rank R f.range + Module.rank R f.ker = Module.rank R MThe theorem at a glance
Rank–Nullity Theorem at a glance
A visual guide to the theorem's hypotheses, structure, and conclusion; the exact statement gives the formal detail.
Rank–Nullity Theorem at a glance
Detailed visual description
The poster separates collapsed kernel directions from the surviving quotient, connects that quotient to the range, and states the exact cardinal-rank theorem without replacing it by a finite matrix example.
Statement structure
Statement and scope
Read the exact Mathlib declaration
This map summarizes the statement's structure; the exact Mathlib declaration remains authoritative.
Rank–Nullity Theorem schematic
Detailed visual description
Parallel kernel-direction fibers foliate the entire domain rather than splitting it into complementary regions. Collapsing each full coset produces the quotient; a central gold equivalence carries those classes to the range, while the encompassing brace relates the kernel and range contributions back to the domain without assuming finite dimension.
Why it matters
A mathematical landmark
Rank–nullity is the structural accounting principle behind linear equations, kernels, images, quotient spaces, and dimension arguments. Mathlib's selected declaration records the stronger cardinal-rank form rather than only the familiar finite-dimensional formula.
ProofAtlas record
What has been checked
Mathlib is the source of the theorem; the local Lean replay and page review are separate.
Claim boundary
No new theorem is claimed
This target indexes Mathlib's cardinal-rank identity for a linear map under its HasRankNullity hypothesis: the ranks of the range and kernel add to the rank of the domain. It is not merely the finite-dimensional natural-number formula and does not claim a new proof.
- Proof Atlas did not originate the Rank–Nullity Theorem or Mathlib's declaration.
- The range is not asserted to equal the codomain, and the map need not be injective or surjective.
- The generated explanation and visuals are not proof evidence.
Source and local evidence
Where the theorem comes from
- Existing declaration
LinearMap.rank_range_add_rank_kerin mathlib- Relationship
- The checked artifact is the upstream declaration itself
- Local Lean evidence
artifact.library.mathlib.rank-nullity-theorem.v001