English
Extensionality principle for ring homomorphisms: if two ring homomorphisms from MonoidAlgebra R M to S agree on singleOneRingHom and on the of embedding, then they are equal.
Русский
Принцип экстенсивности для кольцевых гомоморфизмов: если два гомоморфизма совпадают на singleOneRingHom и на вложение of, то они равны.
LaTeX
$$$\forall f,g: MonoidAlgebra\; R\; M \to+* S, f = g \text{ если } f \circ \operatorname{singleOneRingHom} = g \circ \operatorname{singleOneRingHom} \text{ и } f \circ \operatorname{of} = g \circ \operatorname{of}$$$
Lean4
/-- If two ring homomorphisms from `MonoidAlgebra R M` are equal on all `single m 1`
and `single 1 r`, then they are equal.
See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' [Semiring S] {f g : MonoidAlgebra R M →+* S}
(h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom)
(h_of : (f : MonoidAlgebra R M →* S).comp (of R M) = (g : MonoidAlgebra R M →* S).comp (of R M)) : f = g :=
ringHom_ext (by simpa [DFunLike.ext_iff] using h₁) (by simpa [DFunLike.ext_iff] using h_of)
