Theorems · Theorem · commutative algebra

Algebra.exists_aeval_invOf_eq_zero_of_idealMap_adjoin_sup_span_eq_top

∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S) (I : Ideal R),
  I ≠ ⊤ →
    ∀ [inst_3 : Invertible x],
      Ideal.map (algebraMap R ↥R[x]) I ⊔ Ideal.span {⟨x, ⋯⟩} = ⊤ →
        ∃ p, p.leadingCoeff - 1 ∈ I ∧ (Polynomial.aeval ⅟x) p = 0

Defined in

Mathlib.RingTheory.Polynomial.Ideal

Cited by

3 results in Mathlib

Foundations

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

Assumes

CommRingCommRingAlgebraInvertible