English
If two monoid homomorphisms from a finite product to a common target N agree on all coordinate injections mulSingle i x, they are equal.
Русский
Если два гомоморфизма моноидов из произведения в конечном наборе координат в одно и то же множество N совпадают на каждом инжекте MulSingle i x, то они равны.
LaTeX
$$$$ \\forall i, x:\\, g(\\text{mulSingle}(i,x)) = h(\\text{mulSingle}(i,x)) \\implies g = h. $$$$
Lean4
@[to_additive]
theorem functions_ext [Finite I] (N : Type*) [CommMonoid N] (g h : (∀ i, M i) →* N)
(H : ∀ i x, g (Pi.mulSingle i x) = h (Pi.mulSingle i x)) : g = h :=
by
cases nonempty_fintype I
ext k
rw [← Finset.univ_prod_mulSingle k, map_prod, map_prod]
simp only [H]
