English
If two monoid homomorphisms coincide on all standard basis elements of a finite index family, they are equal.
Русский
Если две моноид-гомоморфные отображения совпадают на всех стандартных базисных элементах конечной индексной семьи, то они равны.
LaTeX
$$$ [Finite ι] [DecidableEq ι] \; {f,g} : (\forall i x, f(\Pi.mulSingle i x) = g(\Pi.mulSingle i x)) \Rightarrow f = g$$$
Lean4
@[to_additive]
theorem _root_.MonoidHom.pi_ext [Finite ι] [DecidableEq ι] {f g : (∀ i, M i) →* γ}
(h : ∀ i x, f (Pi.mulSingle i x) = g (Pi.mulSingle i x)) : f = g :=
by
cases nonempty_fintype ι
ext x
rw [← noncommProd_mul_single x, univ.map_noncommProd, univ.map_noncommProd]
congr 1 with i; exact h i (x i)
