k inj
k) ~ (k!)b inj b) ~ (b!)
k:
. k! = k
(k-1)! 
k,n:. k = n+1 
k! = kn! is mentioned by
| k inj k) ~ (k!) | [nsub_inj_factorial] |
| b inj b) ~ (b!) | [nsub_inj_factorial2] |
| k:. k! = k(k-1)! | [factorial_via_intseg_step_rw] |
| k,n:. k = n+1 k! = kn! | [factorial_via_intseg_step] |
| | [factorial_via_intseg_zero] |
In prior sections: IteratedBinops
Try larger context:
DiscrMathExt
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html