---

Step * 1 2 of Lemma qrng_wf

.....set predicate..... 
IsRing(|<ℚ+*>|;+<ℚ+*>;0;-<ℚ+*>;*;1)
BY
{ (RepUR ``ring_p`` 0 THEN Auto) }

1
IsGroup(ℚ;λx,y. (x + y);0;λx.-(x))

2
1. IsGroup(ℚ;λx,y. (x + y);0;λx.-(x))
⊢ IsMonoid(ℚ;λx,y. (x * y);1)

3
1. IsGroup(ℚ;λx,y. (x + y);0;λx.-(x))
2. IsMonoid(ℚ;λx,y. (x * y);1)
⊢ BiLinear(ℚ;λx,y. (x + y);λx,y. (x * y))

---

Latex:

---

Latex:
.....set  predicate..... 
IsRing(|<\mBbbQ{}+*>|;+<\mBbbQ{}+*>0;-<\mBbbQ{}+*>*;1)


By

---

Latex:
(RepUR  ``ring\_p``  0  THEN  Auto)

---

Home Index