Commit 2023-04-03 16:47 3cacc945

feat(linear_algebra/dimension): free generalizations (#18722) Generalizes many results about module.rank from [division_ring K] to [ring K] [strong_rank_condition K] [module.free K V]. Some lemmas have been moved around in the file to make use of existing variables groupings. There are some lemmas about division rings that I wasn't able to weaken the assumptions on. I'll make the corresponding generalizations to finrank in a follow-up PR.