Commit 2025-07-22 20:14 75b9c0d2

fix(NonZeroDivisors): swap left and right (#27224) Towards #22997 (see also zulip):

• Swap the definitions of nonZeroDivisorsLeft and nonZeroDivisorsRight, so as to conform to the convention in the literature (see https://en.wikipedia.org/wiki/Zero_divisor) and connects to mathlib's IsLeftRegular and IsRightRegular respectively without the presence of commutativity hypotheses.
• Redefine nonZeroDivisors to be the intersection of nonZeroDivisorsLeft and nonZeroDivisorsRight, in analogy with IsRegular.
• Swap Commute.isNilpotent_mul_left/right(_iff) as the names were also contrary to convention. (If the statements are left unchanged then the proofs need to be changed.)