list_prod_map_rpow — Mathlib

English

For any finite list l of NNReal and real r, the product of l's elements raised to r equals the product of l's elements, raised to r.

Русский

Для любого конечного списка l NNReal и вещественного r произведение элементов списка, возведённых в степень r, равно произведению элементов списка, возведённых в степень r.

LaTeX

$$(l.map (·^ r)).prod = l.prod ^ r$$

Lean4

/-- `rpow` variant of `List.prod_map_pow` for `ℝ≥0` -/
theorem list_prod_map_rpow (l : List ℝ≥0) (r : ℝ) : (l.map (· ^ r)).prod = l.prod ^ r :=
  l.prod_hom (rpowMonoidHom r)

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