Theorems · Theorem · commutative algebra

Ideal.exists_nonzero_mem_of_ne_bot

∀ {R : Type u_1} [inst : CommRing R] {P : Ideal (Polynomial R)},
  P ≠ ⊥ →
    (∀ (x : R), Polynomial.C x ∈ P → x = 0) →
      ∃ p ∈ P, Polynomial.map (Ideal.Quotient.mk (Ideal.comap Polynomial.C P)) p ≠ 0

This technical lemma asserts the existence of a polynomial p in an ideal P ⊂ R[x] that is non-zero in the quotient R / (P ∩ R) [x]. The assumptions are equivalent to P ≠ 0 and P ∩ R = (0).

Defined in

Mathlib.RingTheory.Ideal.GoingUp

Cited by

0 results in Mathlib

Foundations

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

Assumes

CommRing