English
If for every coordinate i the compositions g ∘ mulSingle i and h ∘ mulSingle i agree, then g = h.
Русский
Если для каждого i композиции g ∘ mulSingle i и h ∘ mulSingle i совпадают, тогда g=h.
LaTeX
$$$$ \\forall i,\\; g \\circ \\mathrm{mulSingle}_i = h \\circ \\mathrm{mulSingle}_i \\implies g = h. $$$$
Lean4
/-- This is used as the ext lemma instead of `MonoidHom.functions_ext` for reasons explained in
note [partially-applied ext lemmas]. -/
@[to_additive (attr := ext) /-- This is used as the ext lemma instead of `AddMonoidHom.functions_ext` for reasons
explained in note [partially-applied ext lemmas]. -/
]
theorem functions_ext' [Finite I] (N : Type*) [CommMonoid N] (g h : (∀ i, M i) →* N)
(H : ∀ i, g.comp (MonoidHom.mulSingle M i) = h.comp (MonoidHom.mulSingle M i)) : g = h :=
g.functions_ext N h fun i => DFunLike.congr_fun (H i)
