prod_pow — Mathlib

English

For a finite set s and a function f: ι → M, where M is a commutative monoid and n ∈ ℕ, the nth power distributes over the product: ∏_{x ∈ s} f(x)^n = (∏_{x ∈ s} f(x))^n.

Русский

Для конечного множества s и функции f: ι → M в моноиде M выполняется: ∏_{x ∈ s} f(x)^n = (∏_{x ∈ s} f(x))^n, где n ∈ ℕ.

LaTeX

$$$$\prod_{x \in s} f(x)^n = \left(\prod_{x \in s} f(x)\right)^n,$$$$

Lean4

@[to_additive]
theorem prod_pow (s : Finset ι) (n : ℕ) (f : ι → M) : ∏ x ∈ s, f x ^ n = (∏ x ∈ s, f x) ^ n :=
  Multiset.prod_map_pow

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