English
Let g be a finsupp with coefficients in R, b ∈ R and h : α → R → M with h i 0 = 0. Then (b • g).sum h = g.sum (λ i a, h i (b × a)).
Русский
Пусть g — Finsupp α R, и h : α → R → M с h i 0 = 0. Тогда (b • g).sum h = g.sum (λ i a, h i (b × a)).
LaTeX
$$$[MulZeroClass R][AddCommMonoid M] \\; {g : \\alpha \\to_0 R} {b : R} {h : \\alpha \\to R \\to M} (h0 : \\forall i, h i 0 = 0) :\n (b \\cdot g).\\mathrm{sum} h = g.\\mathrm{sum} (\\lambda i a, h i (b \\cdot a))$$$
Lean4
@[to_additive]
theorem mulHom_injective {γ : Type w} [Nonempty I] [∀ i, Mul (f i)] [Mul γ] (g : ∀ i, γ →ₙ* f i)
(hg : ∀ i, Function.Injective (g i)) : Function.Injective (Pi.mulHom g) := fun _ _ h =>
let ⟨i⟩ := ‹Nonempty I›
hg i ((funext_iff.mp h :) i)
