docs(linear_algebra/invariant_basis_number): Drop a TODO (#14973)

This TODO was fixed some time ago by @riccardobrasca, reference the relevant instance in the docstring.

src/linear_algebra/invariant_basis_number.lean

@@ -261,15 +261,11 @@ end
 section
 local attribute [instance] ideal.quotient.field
 
--- TODO: in fact, any nontrivial commutative ring satisfies the strong rank condition.
--- To see this, consider `f : (fin m → R) →ₗ[R] (fin n → R)`,
--- and consider the subring `A` of `R` generated by the matrix entries.
--- That subring is noetherian, and `f` induces a new linear map `f' : (fin m → A) →ₗ[R] (fin n → A)`
--- which is injective if `f` is.
--- Since we've already established the strong rank condition for noetherian rings,
--- this gives the result.
-
-/-- Nontrivial commutative rings have the invariant basis number property. -/
+/-- Nontrivial commutative rings have the invariant basis number property.
+
+In fact, any nontrivial commutative ring satisfies the strong rank condition, see
+`comm_ring_strong_rank_condition`. We prove this instance separately to avoid dependency on
+`linear_algebra.charpoly.basic`. -/
 @[priority 100]
 instance invariant_basis_number_of_nontrivial_of_comm_ring {R : Type u} [comm_ring R]
   [nontrivial R] : invariant_basis_number R :=