prod_mul_pow_card — Mathlib

English

For a finite s and b, the product over s of f(a) multiplied by b^{|s|} equals the product over s of f(a) multiplied by b.

Русский

Для конечного s и b произведение по a∈s f(a), умноженное на b^{|s|}, равно произведению по a∈s (f(a)·b).

LaTeX

$$$\\left(\\prod_{a \\in s} f(a)\\right) \\cdot b^{|s|} = \\prod_{a \\in s} (f(a) \\cdot b)$$$

Lean4

@[to_additive sum_add_card_nsmul]
theorem prod_mul_pow_card {b : M} : (∏ a ∈ s, f a) * b ^ #s = ∏ a ∈ s, f a * b :=
  (Finset.prod_const b).symm ▸ prod_mul_distrib.symm

Похожие утверждения