prod_comp — Mathlib

English

Let R be a domain and p_j ∈ R[X] for j in a finite index set. A root of the product ∏ p_j at x occurs precisely when at least one factor p_i has a root at x; equivalently, IsRoot (∏ p_j) x holds iff ∃ i ∈ index, IsRoot (p_i) x.

Русский

Пусть R — домен, и p_j ∈ R[X]. Корень произведения существует тогда и только тогда, когда хотя бы один фактор имеет корень в x: IsRoot (∏ p_j) x ⇔ ∃ i, IsRoot (p_i) x.

LaTeX

$$$\\text{IsRoot}(\\prod_{j\\in s} p_j, x) \\iff \\exists i\\in s, \\text{IsRoot}(p_i, x)$$$

Lean4

theorem prod_comp {ι : Type*} (s : Finset ι) (p : ι → R[X]) (q : R[X]) :
    (∏ j ∈ s, p j).comp q = ∏ j ∈ s, (p j).comp q :=
  map_prod (compRingHom q) _ _

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