mathlib

7f95e220 - feat(linear_algebra/*): add lemma `linear_independent.finite_of_is_noetherian` (#14714)

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.