English
Let I be a nonempty index set and f i be type-valued semirings. If g i : γ →+* f i are ring homomorphisms that are injective for all i, then the product ring homomorphism Pi.ringHom g is injective.
Русский
Пусть I — непустой индексный набор, для каждого i имеется полукольцо f(i). Если g_i : γ →+* f(i) инъективны для всех i, тогда произведение кольцевых однородных отображений Pi.ringHom g инъективно.
LaTeX
$$$\\text{Injective}(\\Pi.ringHom\\;g)$$$
Lean4
theorem ringHom_injective {γ : Type w} [Nonempty I] [∀ i, NonAssocSemiring (f i)] [NonAssocSemiring γ]
(g : ∀ i, γ →+* f i) (hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.ringHom g) :=
monoidHom_injective (fun i => (g i).toMonoidHom) hg
