Theorems · Theorem · commutative algebra

MvPolynomial.aeval_rename

∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (k : σ → τ) (g : τ → S) (p : MvPolynomial σ R) [inst_2 : Algebra R S],
  (MvPolynomial.aeval g) ((MvPolynomial.rename k) p) = (MvPolynomial.aeval (g ∘ k)) p

Defined in

Mathlib.Algebra.MvPolynomial.Rename

Cited by

9 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiringAlgebra