Theorems · Theorem · commutative algebra

MvPolynomial.map_map

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

Defined in

Mathlib.Algebra.MvPolynomial.Eval

Cited by

2 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringCommSemiring