---

Step * 1 3 of Lemma princ_ideal_wf

.....wf..... 
1. r : Rng
2. a : |r|
3. p : |r| ⟶ ℙ
⊢ istype(p Ideal of r)
BY
{ (Unfold `ideal_p` 0 THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  r  :  Rng
2.  a  :  |r|
3.  p  :  |r|  {}\mrightarrow{}  \mBbbP{}
\mvdash{}  istype(p  Ideal  of  r)


By

---

Latex:
(Unfold  `ideal\_p`  0  THEN  Auto)

---

Home Index