---

Step * of Lemma quot_by_prime_ideal

∀r:CRng. ∀p:Ideal(r){i}. ∀d:detach_fun(|r|;p).  ((∀u:|r|. SqStable(p u)) ⇒ (IsPrimeIdeal(r;p) ⇐⇒ IsIntegDom(r / d)))
BY
{ ((UnivCD) THENA Auto) }

1
1. r : CRng
2. p : Ideal(r){i}
3. d : detach_fun(|r|;p)
4. ∀u:|r|. SqStable(p u)
⊢ IsPrimeIdeal(r;p) ⇐⇒ IsIntegDom(r / d)

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}p:Ideal(r)\{i\}.  \mforall{}d:detach\_fun(|r|;p).
    ((\mforall{}u:|r|.  SqStable(p  u))  {}\mRightarrow{}  (IsPrimeIdeal(r;p)  \mLeftarrow{}{}\mRightarrow{}  IsIntegDom(r  /  d)))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index