Theorems · Theorem · commutative algebra

MvPolynomial.aeval_map_algebraMap

∀ {R : Type u_1} (A : Type u_2) {B : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B]
  (x : σ → B) (p : MvPolynomial σ R),
  (MvPolynomial.aeval x) ((MvPolynomial.map (algebraMap R A)) p) = (MvPolynomial.aeval x) p

Defined in

Mathlib.RingTheory.MvPolynomial.Tower

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiringAlgebraAlgebraAlgebraIsScalarTower