Theorems · Theorem · commutative algebra

MvPolynomial.killCompl_map

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

Defined in

Mathlib.Algebra.MvPolynomial.Rename

Cited by

1 results in Mathlib

Foundations

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

Assumes

CommSemiringCommSemiring