---

Step * of Lemma princ_ideal_mem_cond

∀r:CRng. ∀u,v:|r|.  (v | u in r ⇐⇒ (v)r u)
BY
{ UnivCD 
THENM Unfold `princ_ideal` 0 
THENM Reduce 0 
THENA Auto }

1
1. r : CRng
2. u : |r|
3. v : |r|
⊢ v | u in r ⇐⇒ ∃b:|r|. (u = (v * b) ∈ |r|)

---

Latex:

---

Latex:
\mforall{}r:CRng.  \mforall{}u,v:|r|.    (v  |  u  in  r  \mLeftarrow{}{}\mRightarrow{}  (v)r  u)


By

---

Latex:
UnivCD 
THENM  Unfold  `princ\_ideal`  0 
THENM  Reduce  0 
THENA  Auto

---

Home Index