Theorem AddMonoidHom.mulLeft₃_eq_mulRight₃_iff_associative

Modification history

2025-05-14 08:44
Mathlib/Algebra/Ring/Associator.lean
feat(Algebra/Ring): associator of a non-associative ring (#22823) …
Added AddMonoidHom.mulLeft₃_eq_mulRight₃_iff_associativeView on Github →