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	⊢ Γ = ( exp ∘ log Γ )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cgam	⊢ Γ
1		ce	⊢ exp
2		clgam	⊢ log Γ
3	1 2	ccom	⊢ ( exp ∘ log Γ )
4	0 3	wceq	⊢ Γ = ( exp ∘ log Γ )