m,k:
. 1 
m k 
(k',m':. k' = k-1 m' = m-1 k!m = k
k'!m' 
)f:(A
AA), u:A, a,b:
, e:({a..b
}A).
Thm* a<b
Thm*
Thm* (Iter(f;u) i:{a..b
}. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1))a,b,c,d:. a = b c = d ac = db | Rank | Theorem | Name |
| 3 | m,k:. 1 m k (k',m':. k' = k-1 m' = m-1 k!m = kk'!m' ) | [factorial_tail_via_iter_step] |
| cites the following: | ||
| 1 | f:(AAA), u:A, a,b:, e:({a..b}A).
Thm* a<b Thm*
Thm* (Iter(f;u) i:{a..b }. e(i)) = f((Iter(f;u) i:{a..b-1}. e(i)),e(b-1)) | [iter_via_intseg_split_last] |
| 2 | a,b,c,d:. a = b c = d ac = db | [mul_nat_com] |