Factorial !

The factorial of x is the product of all numbers from (1) to x. It is initially defined as (= (! A) (product (1) A (lambda x x))) /edit/peano/peano_thms.gh/df-factorial. From this definition the recursive definition is derived:

Examples

Arithmetic Overview

Login to edit