finprod_pow — Mathlib

English

If the support of f is finite, then raising the finprod to a natural power n commutes with taking the n-th power inside the product: (∏ᶠ f(i))^n = ∏ᶠ f(i)^n.

Русский

Если опора f конечна, то (∏ᶠ f(i))^n = ∏ᶠ f(i)^n для любого n ∈ ℕ.

LaTeX

$$$\\displaystyle \\left( \\prod\\ᶠ i, f(i) \\right)^n = \\prod\\ᶠ i, f(i)^n$$$

Lean4

@[to_additive]
theorem finprod_pow (hf : (mulSupport f).Finite) (n : ℕ) : (∏ᶠ i, f i) ^ n = ∏ᶠ i, f i ^ n :=
  (powMonoidHom n).map_finprod hf

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