---

Step * 1 1 of Lemma ideal_of_prime


1. r : CRng@i'
2. u : |r|@i
⊢ r-Prime(u) ⇐⇒ (¬u | 1 in r) ∧ (∀a,b:|r|.  (u | a * b in r ⇒ (u | a in r ∨ u | b in r)))
BY
{ Unfold `rprime` 0 THEN Auto }

---

Latex:

---

Latex:

1.  r  :  CRng@i'
2.  u  :  |r|@i
\mvdash{}  r-Prime(u)  \mLeftarrow{}{}\mRightarrow{}  (\mneg{}u  |  1  in  r)  \mwedge{}  (\mforall{}a,b:|r|.    (u  |  a  *  b  in  r  {}\mRightarrow{}  (u  |  a  in  r  \mvee{}  u  |  b  in  r)))


By

---

Latex:
Unfold  `rprime`  0  THEN  Auto

---

Home Index