Commit 2021-05-18 10:47 c2114d45

refactor(linear_algebra/dimension): generalize definition of module.rank (#7634) The main change is to generalize the definition of module.rank. It used to be the infimum over cardinalities of bases, and is now the supremum over cardinalities of linearly independent sets. I have not attempted to systematically generalize theorems about the rank; there is lots more work to be done. For now I've just made a few easy generalizations (either replacing field with division_ring, or division_ring with ring+nontrivial).