Commit 2021-05-21 00:33 53e2307a

feat(ring_theory): every left-noetherian ring has invariant basis number (#7678) This is a lovely case where we get more for less. By directly proving that every left-noetherian ring has invariant basis number, we don't need to import linear_algebra.finite_dimensional in order to do the field case. This means that in a future PR we can instead import ring_theory.invariant_basis_number in linear_algebra.finite_dimensional, and set up the theory of bases in greater generality.