Metamath Proof Explorer
Table of Contents - 5.10.13. Falling and Rising Factorial
- cfallfac
- crisefac
- df-risefac
- df-fallfac
- risefacval
- fallfacval
- risefacval2
- fallfacval2
- fallfacval3
- risefaccllem
- fallfaccllem
- risefaccl
- fallfaccl
- rerisefaccl
- refallfaccl
- nnrisefaccl
- zrisefaccl
- zfallfaccl
- nn0risefaccl
- rprisefaccl
- risefallfac
- fallrisefac
- risefall0lem
- risefac0
- fallfac0
- risefacp1
- fallfacp1
- risefacp1d
- fallfacp1d
- risefac1
- fallfac1
- risefacfac
- fallfacfwd
- 0fallfac
- 0risefac
- binomfallfaclem1
- binomfallfaclem2
- binomfallfac
- binomrisefac
- fallfacval4
- bcfallfac
- fallfacfac