Commit 2022-03-03 19:28 363b7cd9

feat(algebra/ring/basic): generalize lemmas about differences of squares to non-commutative rings (#12366) This copies mul_self_sub_mul_self and mul_self_eq_mul_self_iff to the commute namespace, and reproves the existing lemmas in terms of the new commute lemmas. As a result, the requirements on mul_self_sub_one and mul_self_eq_one_iff and units.inv_eq_self_iff can be weakened from comm_ring to non_unital_non_assoc_ring or ring. This also replaces a few is_domains with the weaker no_zero_divisors, since the lemmas are being moved anyway. In practice this just removes the nontriviality requirements.