map_map — Mathlib

English

The composition of maps on polynomials is compatible with composition of the underlying ring homomorphisms: map g (map f p) = map (g ∘ f) p.

Русский

Сопоставление через два отображения полиномов согласуется с композициями соответствующих гомоморфизмов колец: map g (map f p) = map (g ∘ f) p.

LaTeX

$$$\\mathrm{map}\; g\\bigl(\\mathrm{map}\\; f\\; p\\bigr) = \\mathrm{map}\\; (g \\circ f)\\; p$$$

Lean4

theorem map_map [Semiring T] (g : S →+* T) (p : R[X]) : (p.map f).map g = p.map (g.comp f) :=
  ext (by simp [coeff_map])

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