prod_eq_pow_card — Mathlib

English

Let s be a finite index set and f a function. If f is constant on s, taking the value b for every a in s, then the product over s of f(a) equals b raised to the cardinality of s.

Русский

Пусть s — конечный индексный множитель, и функция f задана на s. Если на s функция f принимает одно и то же значение b, то произведение по a∈s f(a) равно b^{|s|}.

LaTeX

$$$\\bigl(\\forall a \\in s\\; f(a) = b\\bigr) \\Rightarrow \\prod_{a \\in s} f(a) = b^{|s|}$$$

Lean4

@[to_additive sum_eq_card_nsmul]
theorem prod_eq_pow_card {b : M} (hf : ∀ a ∈ s, f a = b) : ∏ a ∈ s, f a = b ^ #s :=
  (prod_congr rfl hf).trans <| prod_const _

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