Def   == {i:| 0i }

is mentioned by

Thm*  m,k:. mk  k!m = ((k!)  ((k-m)!))	[factorial_ratio2]
Thm*  m,k:. mk  k! = (k-m)!k!m	[factorial_ratio]
Thm*  k:. k!	[factorial_via_iter_wf]
Thm*  m,k:. 1  m  k  k!m = k(k-1)!(m-1)	[factorial_tail_via_iter_step_rw]
Thm*  m,k:. 1  m  k  (k',m':. k' = k-1  m' = m-1  k!m = kk'!m'  )	[factorial_tail_via_iter_step]
Thm*  m,k:. k<m  k!m = 0	[factorial_tail_via_iter_zero]
Thm*  m,k:. m = 0    k!m = 1	[factorial_tail_via_iter_null]
Thm*  n,m,k:. nk-m  mk  k!(n+m) = (k-m)!nk!m	[factorial_tail_split_mid]
Thm*  m,k:. k!m	[factorial_tail_via_iter_wf]
Thm*  e:({a..b}). ( i:{a..b}. e(i)) = 1  (i:{a..b}. e(i) = 1)	[iter_nat_prod_one_iff_factors_one]
Thm*  a,b,c:. (ab)c = acbc	[exp_reduce1]
Thm*  i:, x,y:. ixiy = i(x+y)	[sum_exponent]
Thm*  is_ident(; (x,y. x+y); 0)	[natadd_ident_zero]
Thm*  is_ident(; (x,y. xy); 1)	[natmul_ident_one]

In prior sections: int 1 bool 1 int 2 num thy 1 SimpleMulFacts

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html