mathlib3

5ec62c81 - feat(linear_algebra/finrank): generalize finrank to ring in more places (#18716)

feat(linear_algebra/finrank): generalize finrank to ring in more places (#18716) This replaces `[division_ring K]` with the first of the following which compiles: * `[ring K]` * `[ring K] [nontrivial K]` * `[ring K] [strong_rank_condition K]` (implies the previous one via the non-instance `nontrivial_of_invariant_basis_number`)