prod_map_zpow — Mathlib

English

For an integer n, the product of f(i) raised to n over i in m equals the n-th power of the product: (m.map f^n).prod = (m.map f).prod^n.

Русский

Для целого n произведение f(i) в степени n по i из m равно n-ной степени произведения: (m.map f^n).prod = (m.map f).prod^n.

LaTeX

$$$\\big( \\mathrm{map}( \\lambda i, f(i)^n )\\, m \\big).prod = \\big( \\mathrm{prod}( \\mathrm{map} f\, m ) \\big)^n$$$

Lean4

@[to_additive]
theorem prod_map_zpow {n : ℤ} : (m.map fun i => f i ^ n).prod = (m.map f).prod ^ n :=
  by
  convert (m.map f).prod_hom (zpowGroupHom n : G →* G)
  simp only [map_map, Function.comp_apply, zpowGroupHom_apply]

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