# Strong rank condition for commutative rings #

We prove that any nontrivial commutative ring satisfies `StrongRankCondition`

, meaning that
if there is an injective linear map `(Fin n → R) →ₗ[R] Fin m → R`

, then `n ≤ m`

. This implies that
any commutative ring satisfies `InvariantBasisNumber`

: the rank of a finitely generated free
module is well defined.

## Main result #

`commRing_strongRankCondition R`

:`R`

has the`StrongRankCondition`

.

## References #

We follow the proof given in https://mathoverflow.net/a/47846/7845.
The argument is the following: it is enough to prove that for all `n`

, there is no injective linear
map `(Fin (n + 1) → R) →ₗ[R] Fin n → R`

. Given such an `f`

, we get by extension an injective
linear map `g : (Fin (n + 1) → R) →ₗ[R] Fin (n + 1) → R`

. Injectivity implies that `P`

, the
minimal polynomial of `g`

, has non-zero constant term `a₀ ≠ 0`

. But evaluating `0 = P(g)`

at the
vector `(0,...,0,1)`

gives `a₀`

, contradiction.

Any commutative ring satisfies the `StrongRankCondition`

.