English
Given a family of additive monoid homomorphisms f i : A i →+ R that satisfy the necessary unit and multiplicative compatibility conditions, one obtains a RingHom on the direct sum whose values on the injections are the corresponding f i.
Русский
Пусть задано семейство гомоморфизмов A_i →+ R, удовлетворяющее условиям единицы и совместимости умножения; тогда существует кольцевой гомоморфизм на прямом сумме, который ограничивается на i-й компонент как f_i.
LaTeX
$$$$\forall i,x:\ A_i,\quad (toSemiring f\, hone\, hmul)(\operatorname{of} A_i x)=f_i x,$$ где F = toSemiring f hone hmul является кольцевым гомоморфизмом $(\bigoplus_i A_i)\to R$.$$
Lean4
theorem toSemiring_of (f : ∀ i, A i →+ R) (hone hmul) (i : ι) (x : A i) : toSemiring f hone hmul (of _ i x) = f _ x :=
toAddMonoid_of f i x
