Gamma capitalization

Stream: mathlib4

[Violeta Hernández]

I notice that docs#Complex.Gamma, as well as theorems about it, all spell Gamma in uppercase. Does this not go against the naming conventions?

[Thomas Browning]

This seems to go all the way back to this discussion: https://github.com/leanprover-community/mathlib3/pull/12917#pullrequestreview-929584301

[Aaron Liu]

I think there's a thing in the naming convention that says about naming files uppercase unless the file is about a specifically lowercased object. This should fall under an analogous exception for naming things.

[Violeta Hernández]

I mean, we didn't capitalize docs#Ordinal.gamma even though it refers to the same letter with the same capitalization

[Violeta Hernández]

I guess it makes sense to avoid confusing with Euler's γ, though I'd expect that to be called something like eulerGamma or eulerMascheroni anyways.

[Aaron Liu]

docs#Real.eulerMascheroniConstant

[Aaron Liu]

it's not even in the same namespace

[Violeta Hernández]

Aaron Liu said:

it's not even in the same namespace

docs#Real.Gamma

[Aaron Liu]

oh of course yeah why didn't I think of that