---

Step * of Lemma sq_stable__prime_ideal

∀r:CRng. ∀p:Ideal(r){i}.  ((∀u:|r|. Dec(p u)) ⇒ SqStable(IsPrimeIdeal(r;p)))
BY
{ ((UnivCD) THENA Auto) }

1
1. r : CRng@i'
2. p : Ideal(r){i}@i'
3. ∀u:|r|. Dec(p u)@i
⊢ SqStable(IsPrimeIdeal(r;p))

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}p:Ideal(r)\{i\}.    ((\mforall{}u:|r|.  Dec(p  u))  {}\mRightarrow{}  SqStable(IsPrimeIdeal(r;p)))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index