univ_map_map — Mathlib

English

For a ring hom f: R →+* S, mapping the universal polynomial via map f yields the universal polynomial over S: (univ R n).map (MvPolynomial.map f) = univ S n.

Русский

Для гомоморфа f: R →+* S отображение универсального многочлена через map f даёт универсальный многочлен над S: (univ R n).map (MvPolynomial.map f) = univ S n.

LaTeX

$$$(\\mathrm{univ}\,R\,n).map (\\mathrm{MvPolynomial.map} f) = \\mathrm{univ} S n$$$

Lean4

theorem univ_map_map : (univ R n).map (MvPolynomial.map f) = univ S n := by rw [MvPolynomial.map, univ_map_eval₂Hom];
  rfl

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