---

Step * 1 1 1 of Lemma princ_ideal_mem_cond


1. r : CRng
2. u : |r|
3. v : |r|
4. c : |r|
5. (c * v) = u ∈ |r|
⊢ u = (v * c) ∈ |r|
BY
{ (D 1 THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  CRng
2.  u  :  |r|
3.  v  :  |r|
4.  c  :  |r|
5.  (c  *  v)  =  u
\mvdash{}  u  =  (v  *  c)


By

---

Latex:
(D  1  THEN  Auto)

---

Home Index