mathlib

c2114d45 - refactor(linear_algebra/dimension): generalize definition of `module.rank` (#7634)

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`). Co-authored-by: Scott Morrison <scott.morrison@gmail.com>