English
If two ring homomorphisms f and g from the additive monoid algebra R[M] to a semiring S agree on the canonical embedding of R and M into R[M], then f and g are equal.
Русский
Если два кольцевых гомоморфизма f, g: R[M] →+* S совпадают на каноническом внедрении R и M в R[M], то они равны.
LaTeX
$$$\\text{If } f,g: R[M] \\to^* S, \\\\ f\\circ\\iota_R = g\\circ\\iota_R \\text{ and } f\\circ of_{R,M} = g\\circ of_{R,M}, \\text{ then } f=g,$ where $\\iota_R$ and $of_{R,M}$ denote the canonical embeddings.$$
Lean4
/-- If two ring homomorphisms from `R[M]` are equal on all `single m 1`
and `single 0 r`, then they are equal.
See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' [Semiring S] [AddMonoid M] {f g : R[M] →+* S}
(h₁ : f.comp singleZeroRingHom = g.comp singleZeroRingHom)
(h_of : (f : R[M] →* S).comp (of R M) = (g : R[M] →* S).comp (of R M)) : f = g :=
ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)
