map_prod — Mathlib

English

For a list of polynomials, the list product composed with q equals the product of each polynomial composed with q: (List.prod l).comp q = List.prod (List.map (fun p => p.comp q) l).

Русский

Для списка полиномов произведение списка, взятое через композицию с q, равно произведению композиций каждого элемента списка с q.

LaTeX

$$$\\Big(\\text{List}.prod\\ l\\Big).comp q = \\text{List}.prod(\\text{List}.map (\\lambda p, p.comp q)\\ l)$$$

Lean4

protected theorem map_prod {ι : Type*} (g : ι → R[X]) (s : Finset ι) : (∏ i ∈ s, g i).map f = ∏ i ∈ s, (g i).map f :=
  map_prod (mapRingHom f) _ _

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