English
For a nonunital nonassoc semiring, mulLeft a = mulRight a iff ∀ b, Commute a b.
Русский
Для ненулевого ненаследуемого полугруппы: mulLeft a = mulRight a тогда и только тогда, когда ∀ b, a и b коммутируют.
LaTeX
$$$\forall a,\ mulRight a = mulLeft a \iff \forall b,\ Commute(a,b).$$$
Lean4
/-- An `AddMonoidHom` preserves multiplication if pre- and post- composition with
`mul` are equivalent. By converting the statement into an equality of
`AddMonoidHom`s, this lemma allows various specialized `ext` lemmas about `→+` to then be applied.
-/
theorem map_mul_iff (f : R →+ S) :
(∀ x y, f (x * y) = f x * f y) ↔ (mul : R →+ R →+ R).compr₂ f = (mul.comp f).compl₂ f :=
Iff.symm ext_iff₂
