mathlib3

86766851 - feat(ring_theory): every left-noetherian ring satisfies the strong rank condition (#7711)

feat(ring_theory): every left-noetherian ring satisfies the strong rank condition (#7711) This PR also discards the proof that every left-noetherian ring satisfies the rank condition, because we already have in #7683 that this implies that. Co-authored-by: Scott Morrison <scott.morrison@gmail.com> Co-authored-by: Johan Commelin <johan@commelin.net>