multiset_prod_comp — Mathlib

English

Evaluation commutes with composition under finite products: the evaluation of the product over a finite set of polynomials, composed with q, equals the product over the same set of the compositions: (∏ j∈s p_j).comp q = ∏ j∈s (p_j).comp q.

Русский

Оценивание произведения полиномов, взятое через композицию c q, равно произведению композиций каждого полинома: (∏ p_j).comp q = ∏ (p_j).comp q.

LaTeX

$$$\\left(\\prod_{j\\in s} p_j\\right).comp\\ q = \\prod_{j\\in s} (p_j).comp\\ q$$$

Lean4

theorem multiset_prod_comp (s : Multiset R[X]) (q : R[X]) : s.prod.comp q = (s.map fun p : R[X] => p.comp q).prod :=
  map_multiset_prod (compRingHom q) _

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