namespace when no dot notation available

Stream: mathlib4

[Kevin Buzzard]

In #14134 a new definition (in fact an abbrev) ringKrullDim R : WithBot (WithTop ℕ) is made. Where do theorems about this definition go? There will not be an opportunity to use dot notation. Right now in the PR they've been put in a ringKrullDim namespace anyway, but when I look at definitions like finprod which also can't be used with dot notation, all the theorems are just called finprod_foo in the root namespace. Should this also be the approach here?

[Damiano Testa]

Would this be eligible for "anonymous" dot-notation? That can be quite useful, I find.

[Damiano Testa]

I think that there was a recent thread about possibly renaming mathlib3's foo_something with foo.something even if dot-notation would not be applicable precisely to allow "anonymous" dot-notation.

[Kevin Buzzard]

I'm not sure what you mean. Can anonymous dot notation somehow play a role when ringKrullDim R is a term of a non-Prop type?

[Andrew Yang]

IIRC we almost never use namespaces for non-Sort-valued definitions.

[Damiano Testa]

Ah, you are right! I had it in my mind that it was kd_le!! My comment was misguided.

[Markus Himmel]

Andrew Yang said:

IIRC we almost never use namespaces for non-Sort-valued definitions.

I don't think this is true. On my mathlib checkout, rg -c '^namespace (.*\.)?[a-z]+[A-Z]' | wc -l returns 84, which means that there are 84 files which contain something like namespace legendreSymbol.

[Eric Wieser]

Some of these are the gray area of "non-sorts with a coercion to Sort", like docs#unitary

[Yaël Dillies]

and namespacing stuff about docs#multiplicity seems like it is a mistake

[Kyle Miller]

Generally in programming namespacing is a good thing. Dot notation isn't the only reason to namespace (and historically namespaces came before dot notation). For one, everything has a well-defined prefix and so you have, for example tab completion. For another, it helps keeps names from colliding between different parts of the library.

Namespacing also gives you the option to decide to open the namespace and get access to all the names without the prefix. Without namespacing, it's like you're telling everyone that they should always open this namespace.

[Yaël Dillies]

Yes but lemmas aren't usually about a single non-Sort def and, when they are, where such non-Sort def appears in the expression is relevant and should be reflected in the name. Putting the lemma in the namespace of the non-Sort just is too crude

[Yaël Dillies]

You can however do def Namespace.nonSortDef, lemma Namespace.lemma_about_nonSortDef (rather than the def nonSortDef, lemma nonSortDef.lemma_about you seem to be arguing for)