Dimension characterizes isomorphism

For every field $K$ and every pair of types $V$ and $W$ (in arbitrary universes) that are each equipped with the structure of an additive commutative group together with a $K$-module structure, and each assumed to be finite-dimensional over $K$ — all of these being instance-level assumptions supplied implicitly, with the same field $K$ acting on both $V$ and $W$ — the statement asserts the following biconditional (an "if and only if", not a one-directional implication):

Here the left-hand side is the assertion that the type of $K$-linear equivalences from $V$ to $W$ — i.e. $K$-linear maps $f : V \to W$ that are bijective, with a specified two-sided inverse that is itself $K$-linear — is inhabited; it is a bare existence claim ("the collection of such isomorphisms is nonempty"), with no uniqueness, no canonicity, and no particular isomorphism named or constructed. The right-hand side is an equality of natural numbers: $\dim_K V$ and $\dim_K W$ denote Mathlib's Module.finrank, the rank of the module as a natural number, and under the standing finite-dimensionality hypotheses these coincide with the ordinary dimensions (the convention by which finrank returns $0$ for an infinite-dimensional space is not in play here, since both spaces are assumed finite-dimensional; note, however, that $0$ remains the genuine value in the degenerate case where $V$ or $W$ is the zero module). The quantification silently includes all degenerate cases: $V$ and/or $W$ may be the trivial module $\{0\}$, in which case the right-hand side reads $0 = 0$ and the left-hand side is witnessed by the zero map; $V$ and $W$ may be the same space, or literally the same type; and $K$ may be any field whatsoever, including finite fields and fields of positive characteristic. No hypothesis relates $V$ and $W$ beyond their sharing the scalar field $K$ and both being finite-dimensional, and every stated hypothesis is satisfiable (e.g. $V = W = K$), so the statement is not vacuous. Nothing is asserted about bases, matrices, or coordinates, and no explicit universally quantified term-level variables appear — the only variables are the two module types, the field, and their structural instances. The declaration is stated inside a namespace and its proof is left unfilled (sorry), so the file asserts the biconditional as a claim without supplying a proof of it.