Commit 2023-11-08 18:36 d34f0e9a

View on Github →

chore: add basic @[simp]s for Gamma (#7977) I don't personally have any need for these. It just seemed like these would make the API more complete.

Estimated changes

Modified Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean

added theorem Complex.Gamma_ofNat_eq_factorial

modified theorem Complex.Gamma_one

added theorem Real.Gamma_ofNat_eq_factorial

Modified Mathlib/Analysis/SpecialFunctions/Gamma/BohrMollerup.lean

modified theorem Real.Gamma_two