English
Let s be a Finset of N, b: N → M and f: N → N with MulDistribMulAction. Then ∏ i∈s, b i • f i = (∏ i∈s, b i) • (∏ i∈s, f i).
Русский
Пусть s — Finset, b:i→M, f:i→N; тогда произведение по i в s: ∏ (b i • f i) = (∏ b i) • (∏ f i).
LaTeX
$$$\\forall {M} {N} [\\mathsf{Monoid} M] [\\mathsf{CommMonoid} N] [\\mathsf{MulAction} M N] [\\mathsf{IsScalarTower} M N N] [\\mathsf{SMulCommClass} M N N] (s:\\mathsf{Finset} N) (b:N\\to M) (f:N\\to N),\\; \\prod i\\in s, b i \\cdot f i = (\\prod i\\in s, b i) \\cdot (\\prod i\\in s, f i)$$$
Lean4
theorem prod_smul [CommMonoid N] [CommMonoid M] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N]
(s : Finset N) (b : N → M) (f : N → N) : ∏ i ∈ s, b i • f i = (∏ i ∈ s, b i) • ∏ i ∈ s, f i := by
induction s using Finset.cons_induction_on with
| empty => simp
| cons _ _ hj ih => rw [prod_cons, ih, smul_mul_smul_comm, ← prod_cons hj, ← prod_cons hj]
