English
Let R be a nonunital, nonassociative semiring. The two natural three-fold multiplications mulLeft₃ and mulRight₃ agree if and only if the binary operation is associative; equivalently, (x·y)·z = x·(y·z) for all x,y,z in R.
Русский
Пусть R — ненулевой ненаследующий полугрупповый полуг ring? без единицы и без ассоциативности. Равенство двух троичных умножений mulLeft₃ и mulRight₃ допускается тогда и только тогда, когда умножение ассоциативно; то есть для всех x,y,z ∈ R выполняется (x·y)·z = x·(y·z).
LaTeX
$$$mulLeft_3\,(R := R) = mulRight_3 \iff \forall x,y,z \in R,\ (x\cdot y)\cdot z = x\cdot (y\cdot z).$$$
Lean4
/-- An a priori non-associative semiring is associative if the `AddMonoidHom` versions of
the multiplications `(x * y) * z` and `x * (y * z)` agree. -/
theorem mulLeft₃_eq_mulRight₃_iff_associative : mulLeft₃ (R := R) = mulRight₃ ↔ Std.Associative (fun (x y : R) ↦ x * y)
where
mp h := ⟨fun x y z ↦ by rw [← mulLeft₃_apply, ← mulRight₃_apply, h]⟩
mpr h := by ext x y z; simp [Std.Associative.assoc]
