| Who Cites qadd? |
|
qadd | Def a +q b == (a.numb.den+b.numa.den)/(a.denb.den) |
| | Thm* p,q:. p +q q |
|
qdenom | Def q.den == 2of(q) |
| | Thm* q:. q.den |
|
qnumer | Def q.num == 1of(q) |
| | Thm* q:. q.num |
|
qnum | Def p/q == <p,q> |
| | Thm* n:, d:. n/d |
|
pi2 | Def 2of(t) == t.2 |
| | Thm* A:Type, B:(AType), p:(a:AB(a)). 2of(p) B(1of(p)) |
|
pi1 | Def 1of(t) == t.1 |
| | Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A |