Theorems · Theorem · commutative algebra

Polynomial.erase_mem_lifts

∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S} (n : ℕ),
  p ∈ Polynomial.lifts f → Polynomial.erase n p ∈ Polynomial.lifts f

If p lifts then p.erase n lifts.

Defined in

Mathlib.Algebra.Polynomial.Lifts

Cited by

0 results in Mathlib

Foundations

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

Assumes

SemiringSemiring