Capitalisation

Stream: mathlib4

[David Loeffler]

Am I correct that quotientAddGroup.btw_coe_iff, and other lemma names of the shape quotientAddGroup.xxx, are typos and should be QuotientAddGroup.xxx? Just checking because I'm not quite sure I've understood the conventions for upper/lowercase names in mathlib4.

[Mario Carneiro]

Namespaces (i.e. every name component except the last) are almost always capital camel case. The only exception is when defining local let recs (since those are in the namespace of the containing function) and theorems which use dot-notation, applied to something that is not capital camel case (this would only happen if there is a non-prop thing that can be coerced to a type, since props and types are also capital camel case).

[Eric Wieser]

and theorems which use dot-notation, applied to something that is not capital camel case (this would only happen if there is a non-prop thing that can be coerced to a type, since props and types are also capital camel case).

Does dot notation actually work in these cases anyway?