Commit 2025-05-14 08:44 c53aaa67

feat(Algebra/Ring): associator of a non-associative ring (#22823) If R is a non-associative ring, then (x * y) * z - x * (y * z) is called the associator of ring elements x y z : R. The associator vanishes exactly when R is associative. We prove variants of this statement also for the AddMonoidHom bundled version of the associator, as well as the bundled version of mulLeft₃ and mulRight₃, the multiplications (x * y) * z and x * (y * z).