map_multiset_prod — Mathlib

English

The product of a multiset of polynomials, composed with q, equals the product of the compositions of each p with q: s.prod (p_i).comp q.

Русский

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

LaTeX

$$$s.prod (\\lambda i, p_i).comp q = (s.map (\\lambda p, p.comp q)).prod$$$

Lean4

protected theorem map_multiset_prod (m : Multiset R[X]) : m.prod.map f = (m.map <| map f).prod :=
  Eq.symm <| Multiset.prod_hom _ (mapRingHom f).toMonoidHom

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