Fungrim entry: 81aeba

Symbol: Factorial —

n !

— Factorial

Domain	Codomain
$n \in \mathbb{Z}_{\ge 0}$	$n ! \in \mathbb{Z}_{\ge 1}$

Table data:

\left(P, Q\right)

such that

\left(P\right) \;\implies\; \left(Q\right)

Definitions:

Fungrim symbol	Notation	Short description
`Factorial`	$n !$	Factorial
`ZZGreaterEqual`	$\mathbb{Z}_{\ge n}$	Integers greater than or equal to n

Source code for this entry:

Entry(ID("81aeba"),
    SymbolDefinition(Factorial, Factorial(n), "Factorial"),
    Table(TableRelation(Tuple(P, Q), Implies(P, Q)), TableHeadings(Description("Domain"), Description("Codomain")), List(Tuple(Element(n, ZZGreaterEqual(0)), Element(Factorial(n), ZZGreaterEqual(1))))))

Topics using this entry

Factorials and binomial coefficients

Copyright (C) Fredrik Johansson and contributors. Fungrim is provided under the MIT license. The source code is on GitHub.

2021-03-15 19:12:00.328586 UTC