English
If two ring homomorphisms from SkewMonoidAlgebra k G to k agree on all single 1 b and all single a 1, then they are equal.
Русский
Если два кольцевых гомоморфизма из SkewMonoidAlgebra k G в k совпадают на всех элементах вида single 1 b и single a 1, то они равны.
LaTeX
$$$\forall b:\ f (single\;1\; b) = g (single\;1\; b) \land \forall a:\ f (single\; a\; 1) = g (single\; a\; 1) \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. -/
theorem ringHom_ext {f g : SkewMonoidAlgebra k G →+* k} (h₁ : ∀ b, f (single 1 b) = g (single 1 b))
(h_of : ∀ a, f (single a 1) = g (single a 1)) : f = g :=
have {a : G} {b₁ b₂ : k} : (single 1 b₁) * (single a b₂) = single a (b₁ * b₂) := by
simp [single_mul_single, one_mul, one_smul]
RingHom.coe_addMonoidHom_injective <|
addHom_ext fun a b ↦ by
rw [← mul_one b, ← this, AddMonoidHom.coe_coe f, AddMonoidHom.coe_coe g, f.map_mul, g.map_mul, h₁, h_of]
