English
Let F,G be ring homomorphisms from the direct sum ⨁i A_i to R. If for every index i the two maps agree on the i-th component, i.e., F ∘ in_i = G ∘ in_i, then F = G.
Русский
Пусть F,G -- кольцевые гомоморфизмы из прямого суммы ⨁i A_i в R. Если для каждого индекса i они совпадают на i-й компоненте, то F = G.
LaTeX
$$$$\text{Let }F,G:(\bigoplus_i A_i)\to R\text{ be ring homomorphisms. If }\forall i,\ F\circ \iota_i = G\circ \iota_i,\ \text{then } F=G.$$$$
Lean4
/-- If two ring homomorphisms from `⨁ i, A i` are equal on each `of A i y`,
then they are equal.
See note [partially-applied ext lemmas]. -/
@[ext]
theorem ringHom_ext' ⦃F G : (⨁ i, A i) →+* R⦄ (h : ∀ i, (↑F : _ →+ R).comp (of A i) = (↑G : _ →+ R).comp (of A i)) :
F = G :=
RingHom.coe_addMonoidHom_injective <| DirectSum.addHom_ext' h
