Theorems · Definition · commutative algebra

MvPolynomial.aeval

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

A map σ → S₁ where S₁ is an algebra over R generates an R-algebra homomorphism from multivariate polynomials over σ to S₁.

Defined in

Mathlib.Algebra.MvPolynomial.Eval

Cited by

298 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebra