prod_zpow — Mathlib

English

For a Division Commutative Monoid, taking integer powers commutes with taking the product over a list: the product of x^r over all x in l equals (l.prod)^r.

Русский

В коммутативном делении моноида для целочисленных степеней произведение x^r по всем x в списке равно (произведение списка)^r.

LaTeX

$$$l.prod^{\, r} = (l.map (\\lambda x, x^{r})).prod$$

Lean4

theorem prod_zpow {β : Type*} [DivisionCommMonoid β] {r : ℤ} {l : List β} : l.prod ^ r = (map (fun x ↦ x ^ r) l).prod :=
  let fr : β →* β := ⟨⟨fun b ↦ b ^ r, one_zpow r⟩, (mul_zpow · · r)⟩
  map_list_prod fr l

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