Theorems · Theorem · commutative algebra

MvPolynomial.map_aeval

∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] [inst_2 : Algebra R S₁]
  {B : Type u_2} [inst_3 : CommSemiring B] (g : σ → S₁) (φ : S₁ →+* B) (p : MvPolynomial σ R),
  φ ((MvPolynomial.aeval g) p) = (MvPolynomial.eval₂Hom (φ.comp (algebraMap R S₁)) fun i => φ (g i)) p

Defined in

Mathlib.Algebra.MvPolynomial.Eval

Cited by

19 results in Mathlib

Foundations

Depth 96 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CommSemiringCommSemiringAlgebraCommSemiring