Theorems · Theorem · commutative algebra

MvPolynomial.rename_rename

∀ {σ : Type u_1} {τ : Type u_2} {α : Type u_3} {R : Type u_4} [inst : CommSemiring R] (f : σ → τ) (g : τ → α)
  (p : MvPolynomial σ R), (MvPolynomial.rename g) ((MvPolynomial.rename f) p) = (MvPolynomial.rename (g ∘ f)) p

Defined in

Mathlib.Algebra.MvPolynomial.Rename

Cited by

13 results in Mathlib

Foundations

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

Assumes

CommSemiring