Theorems · Theorem · commutative algebra

MvPolynomial.map_rename

∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* S) (g : σ → τ) (p : MvPolynomial σ R),
  (MvPolynomial.map f) ((MvPolynomial.rename g) p) = (MvPolynomial.rename g) ((MvPolynomial.map f) p)

Defined in

Mathlib.Algebra.MvPolynomial.Rename

Cited by

8 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiring