Commit 2022-07-01 18:31 7f95e220
View on Github →feat(linear_algebra/*): add lemma linear_independent.finite_of_is_noetherian (#14714)
This replaces fintype_of_is_noetherian_linear_independent which gave the same
conclusion except demanded strong_rank_condition R instead of just nontrivial R.
Also some other minor gaps filled.