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
-
(= (! (0)) (1)) /edit/peano/peano_thms.gh/factorial0
-
(= (! (1)) (1)) /edit/peano/peano_thms.gh/factorial1
-
(/\ (= (! (2)) (* (1) (2))) (= (* (1) (2)) (2))) /edit/peano/arithmetic.gh/factorial2
-
(/\ (= (! (3)) (* (* (1) (2)) (3))) (= (* (* (1) (2)) (3)) (6))) /edit/peano/arithmetic.gh/factorial3
-
(/\ (= (! (4)) (* (* (* (1) (2)) (3)) (4))) (= (* (* (* (1) (2)) (3)) (4)) (+ (* (2) (10)) (4)) )) /edit/peano/arithmetic.gh/factorial4
-
(/\ (= (! (5)) (* (* (* (* (1) (2)) (3)) (4)) (5))) (= (* (* (* (* (1) (2)) (3)) (4)) (5)) (+ (* (10) (10)) (* (2) (10))) )) /edit/peano/arithmetic.gh/factorial5
-
(/\ (= (! (6)) (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6))) (= (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (+ (* (7) (* (10) (10))) (* (2) (10))) )) /edit/peano/arithmetic.gh/factorial6
-
(/\ (= (! (7)) (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7))) (= (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7)) (+ (* (5) (* (10) (* (10) (10)))) (* (4) (10))) )) /edit/peano/arithmetic.gh/factorial7
-
(/\ (= (! (8)) (* (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7)) (8))) (= (* (* (* (* (* (* (* (1) (2)) (3)) (4)) (5)) (6)) (7)) (8)) (+ (* (4) (* (10) (* (10) (* (10) (10))))) (+ (* (3) (* (10) (10))) (* (2) (10)))) )) /edit/peano/arithmetic.gh/factorial8
Arithmetic Overview
