mathlib

363b7cd9 - feat(algebra/ring/basic): generalize lemmas about differences of squares to non-commutative rings (#12366)

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_domain`s with the weaker `no_zero_divisors`, since the lemmas are being moved anyway. In practice this just removes the nontriviality requirements.