Theorems · Definition · field theory

Polynomial.map

{R : Type u} → {S : Type v} → [inst : Semiring R] → [inst_1 : Semiring S] → (R →+* S) → Polynomial R → Polynomial S

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

Defined in

Mathlib.Algebra.Polynomial.Eval.Defs

Cited by

806 results in Mathlib

Foundations

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

Assumes

SemiringSemiring