Metamath Proof Explorer

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 
|- _G = ( exp o. log_G )

Detailed syntax breakdown

Step Hyp Ref Expression
0 cgam 
 |-  _G
1 ce 
 |-  exp
2 clgam 
 |-  log_G
3 1 2 ccom 
 |-  ( exp o. log_G )
4 0 3 wceq 
 |-  _G = ( exp o. log_G )