| Who Cites reduce factorization? |
|
reduce_factorization | Def reduce_factorization(f; j)(i) == if i=j f(i)-1 else f(i) fi |
| | Thm* a,b:, f:({a..b}), j:{a..b}.
Thm* 0<f(j) reduce_factorization(f; j) {a..b} |
|
eq_int | Def i=j == if i=j true ; false fi |
| | Thm* i,j:. (i=j) |