completion should be capitalized?

Stream: mathlib4

[Kevin Buzzard]

I still wouldn't say I was 100% on the Lean 4 naming convention, but one thing that has sunk in is that terms begin with small letters and types begin with capitals. So should docs#NumberField.InfinitePlace.completion and docs#AbsoluteValue.completion both be ...Completion? Asking before I PR.

[Mario Carneiro]

yes, especially since all of the definitions after it seem to be in the capitalized namespace

[Kevin Buzzard]

#19646

[Kevin Buzzard]

Mario Carneiro said:

yes, especially since all of the definitions after it seem to be in the capitalized namespace

In fact, that was what alerted me to it! (the clue was the first lemma here )