Read-back: HefferonLinAlg.rank_plus_nullity

For every field $K$ and every pair of types $V$ and $W$ (at arbitrary universe levels) that are each equipped with the structure of an additive commutative group together with a $K$-module structure, and under the additional standing assumption that $V$ is a finite-dimensional $K$-vector space (no finiteness whatsoever is assumed of $W$, which may be infinite-dimensional or zero), the claim is that for every $K$-linear map $f \colon V \to W$ the equation

holds, where: $\operatorname{im} f = \{f(v) : v \in V\}$ is the image submodule of $W$ and $\ker f = \{v \in V : f(v) = 0\}$ is the kernel submodule of $V$, each regarded as a $K$-module in its own right; each of the three occurrences of $\dim_K$ is the natural-number-valued rank function Module.finrank (the cardinality of a basis, which by convention returns the junk value $0$ for a module that is not finite-dimensional — a case that cannot arise here, since $V$ finite-dimensional forces both the kernel, as a submodule of $V$, and the image, as a quotient-like image of $V$, to be finite-dimensional as well); and the sum on the left is ordinary addition of natural numbers, so the equation is an identity in $\mathbb{N}$ rather than in $\mathbb{Z}$ or a cardinal arithmetic. The statement is universally quantified over $K$, $V$, $W$, all four typeclass structures listed above, the finite-dimensionality hypothesis on $V$, and the map $f$; there are no other hypotheses, in particular no injectivity, surjectivity, or nondegeneracy assumption on $f$, and no assumption that $V$ or $W$ is nonzero. Degenerate instances are therefore included: when $V = 0$ the assertion reads $0 + 0 = 0$; when $f$ is the zero map it reads $0 + \dim_K V = \dim_K V$; when $f$ is injective it reads $\dim_K(\operatorname{im} f) + 0 = \dim_K V$; and when $W = 0$ it likewise reads $0 + \dim_K V = \dim_K V$. Note that the summand order is image-rank first and kernel-rank second, and that the equality is an unconditional equality of the two natural numbers, not an inequality or a bound in either direction. The declaration is stated inside the namespace HefferonLinAlg, and its proof is left as sorry, i.e. the file contains no proof of this claim.