Commit 2022-05-03 19:18 5cfb8dbc

refactor(ring_theory/jacobson_ideal): generalize lemmas to non-commutative rings (#13865) The main change here is that the order of multiplication has been adjusted slightly in mem_jacobson_iffand exists_mul_sub_mem_of_sub_one_mem_jacobson. In the commutative case this doesn't matter anyway. All the other changes are just moving lemmas between sections, the statements of no lemmas other than those two have been changed. No lemmas have been added or removed. The lemmas about is_unit and quotients don't generalize as easily, so I've not attempted to touch those; that would require some mathematical insight, which is out of scope for this PR!