Theorems · Definition · commutative algebra

MvPolynomial.map

{R : Type u} →
  {S₁ : Type v} →
    {σ : Type u_1} →
      [inst : CommSemiring R] → [inst_1 : CommSemiring S₁] → (R →+* S₁) → MvPolynomial σ R →+* MvPolynomial σ S₁

map f p maps a polynomial p across a ring hom f

Defined in

Mathlib.Algebra.MvPolynomial.Eval

Cited by

147 results in Mathlib

Foundations

Depth 81 from the axioms, rests on 1,708 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiring