English
If two ring homomorphisms from SkewMonoidAlgebra k G to k agree on the two basic generators, then the homomorphisms are equal.
Русский
Если два кольцевых гомоморфизма из SkewMonoidAlgebra k G в k совпадают на двух базисных генераторах, то гомоморфизмы равны.
LaTeX
$$$\forall f,g:\ SkewMonoidAlgebra k G \to^+_* k,\ (f\circ singleOneRingHom) = (g\circ singleOneRingHom) \/\&\& (f \circ (of k G)) = (g \circ (of k G)) \Rightarrow f = g$$$
Lean4
/-- If two ring homomorphisms from `SkewMonoidAlgebra k G` are equal on all `single a 1`
and `single 1 b`, then they are equal.
See note [partially-applied ext lemmas]. -/
@[ext high]
theorem ringHom_ext' {f g : SkewMonoidAlgebra k G →+* k} (h₁ : f.comp singleOneRingHom = g.comp singleOneRingHom)
(h_of : (f : SkewMonoidAlgebra k G →* k).comp (of k G) = (g : SkewMonoidAlgebra k G →* k).comp (of k G)) : f = g :=
ringHom_ext (RingHom.congr_fun h₁) (DFunLike.congr_fun h_of)
