Theorems · Definition · field theory

Polynomial.aeval

{R : Type u} →
  {A : Type z} → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A → Polynomial R →ₐ[R] A

Given a valuation x of the variable in an R-algebra A, aeval R A x is the unique R-algebra homomorphism from R[X] to A sending X to x. This is a stronger variant of the linear map Polynomial.leval.

Defined in

Mathlib.Algebra.Polynomial.AlgebraMap

Cited by

615 results in Mathlib

Foundations

Depth 109 from the axioms, rests on 2,018 definitions · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringSemiringAlgebra