pow_card_mul_prod — Mathlib

English

For a finite s and elements b and values f(a), multiplying by b in each factor is equivalent to multiplying the whole product by b raised to the power |s|.

Русский

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

LaTeX

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

Lean4

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

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