English
For Finset s of N with M-action, the Finset product distributes over the pointwise action: ∏ i∈s, b i • f i = (∏ i∈s, b i) • ∏ i∈s, f i.
Русский
Для Finset s над N с действием M скалярно: произведение по i ∈ s равно произведению b_i домноженного на f_i, т.е. (∏ b_i) • (∏ f_i).
LaTeX
$$$\\forall {M} {N} [\\mathsf{Monoid} M] [\\mathsf{CommMonoid} N] [\\mathsf{MulDistribMulAction} M N] (s:\\mathsf{Finset} N) (b: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 smul_prod [CommMonoid N] [Monoid M] [MulAction M N] [IsScalarTower M N N] [SMulCommClass M N N] (s : Finset N)
(b : M) (f : N → N) : b ^ s.card • ∏ x ∈ s, f x = ∏ x ∈ s, b • f x :=
by
have : Multiset.map (fun (x : N) ↦ b • f x) s.val = Multiset.map (fun x ↦ b • x) (Multiset.map f s.val) := by
simp only [Multiset.map_map, Function.comp_apply]
simp_rw [prod_eq_multiset_prod, card_def, this, ← Multiset.smul_prod _ b, Multiset.card_map]
