---

Step * 1 2 1 of Lemma princ_ideal_wf


1. r : Rng
2. a : |r|
⊢ ∃b:|r|. (0 = (a * b) ∈ |r|)
BY
{ TACTIC:(With ⌜0⌝ (D 0)⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  r  :  Rng
2.  a  :  |r|
\mvdash{}  \mexists{}b:|r|.  (0  =  (a  *  b))


By

---

Latex:
TACTIC:(With  \mkleeneopen{}0\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)

---

Home Index