Theorems · Theorem · commutative algebra

MvPolynomial.eval_map

∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (g : σ → S₁) (p : MvPolynomial σ R), (MvPolynomial.eval g) ((MvPolynomial.map f) p) = MvPolynomial.eval₂ f g p

Defined in

Mathlib.Algebra.MvPolynomial.Eval

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiring