---

Step * 1 of Lemma sq_stable__prime_ideal


1. r : CRng@i'
2. p : Ideal(r){i}@i'
3. ∀u:|r|. Dec(p u)@i
⊢ SqStable(IsPrimeIdeal(r;p))
BY
{ Unfold `prime_ideal_p` 0 
THEN ProveSqStable1 
THENA Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
Unfold  `prime\_ideal\_p`  0 
THEN  ProveSqStable1 
THENA  Auto

---

Home Index