n,m,k:
. n
k-m 
mk k!(n+m) = (k-m)!n
k!ma,c,b:
, e:({a..b
}
).
Thm* a
c
Thm*
Thm* c
b (
i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i))| Rank | Theorem | Name |
| 4 | n,m,k:. nk-m mk k!(n+m) = (k-m)!nk!m | [factorial_tail_split_mid] |
| cites the following: | ||
| 3 | a,c,b:, e:({a..b}).
Thm* a c
Thm*
Thm* c b ( i:{a..b}. e(i)) = ( i:{a..c}. e(i))( i:{c..b}. e(i)) | [mul_via_intseg_split_mid] |