| 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)  |