English
The map induces a homomorphism that transports a polynomial p ∈ MvPolynomial σ R to MvPolynomial σ S1 by applying f to coefficients and leaving the indeterminates X intact.
Русский
Map вызывает гомоморфизм, переводящий полином p ∈ MvPolynomial σ R в MvPolynomial σ S1, применяя f к коэффициентам и сохраняя переменные X без изменений.
LaTeX
$$$\\mathrm{map}_{f} : \\! MvPolynomial\\ σ\\ R \\to MvPolynomial\\ σ\\ S1 ,\\; \\mathrm{map}_{f}(p) = \\mathrm{eval}_2\\bigl(\\mathrm{C} \\circ f, \\mathrm{X}\\bigr)(p)$$$
Lean4
/-- `map f p` maps a polynomial `p` across a ring hom `f` -/
def map : MvPolynomial σ R →+* MvPolynomial σ S₁ :=
eval₂Hom (C.comp f) X
