prod_zpow — Mathlib

English

For a finite set s and a function f: ι → G into a division monoid G, and integer exponent n, ∏_{a∈s} f(a)^n = (∏_{a∈s} f(a))^n.

Русский

Для конечного множества s и функции f: ι → G в моноид деления, и целочисленного показателя n, имеем ∏ f(a)^n = (∏ f(a))^n.

LaTeX

$$$$\prod_{a \in s} f(a)^n = \left(\prod_{a \in s} f(a)\right)^n.$$$$

Lean4

@[to_additive]
theorem prod_zpow (f : ι → G) (s : Finset ι) (n : ℤ) : ∏ a ∈ s, f a ^ n = (∏ a ∈ s, f a) ^ n :=
  Multiset.prod_map_zpow

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