Definition df-gam

Description: Define the Gamma function. See df-lgam for more information about the reason for this definition in terms of the log-gamma function. (Contributed by Mario Carneiro, 12-Jul-2014)

	Ref	Expression
Assertion	df-gam	$$⊢\mathrm{\Gamma }=\exp \circ \log \mathrm{\Gamma }$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgam	$$class\mathrm{\Gamma }$$
1		ce	$$class\exp$$
2		clgam	$$class\log \mathrm{\Gamma }$$
3	1 2	ccom	$$class\left(\exp \circ \log \mathrm{\Gamma }\right)$$
4	0 3	wceq	$$wff\mathrm{\Gamma }=\exp \circ \log \mathrm{\Gamma }$$