IteratedBinops
Sections
DiscrMathExt
Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Rank
Theorem
Name
7
Thm*
k
:
.
k
!
[factorial_via_iter_wf]
cites the following:
6
Thm*
(
i
:{
a
..
b
}.
e
(
i
)) = 0
(
i
:{
a
..
b
}.
e
(
i
) = 0)
[iter_prod_zero_iff_factor_zero]
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
IteratedBinops
Sections
DiscrMathExt
Doc
k:
. k! 
i:{a..b
}. e(i)) = 0 
(
i:{a..b}. e(i) = 0)k:. k! i:{a..b}. e(i)) = 0 (i:{a..b}. e(i) = 0)