## Stream: maths

### Topic: localization

#### Johan Commelin (Mar 05 2019 at 08:58):

Currently we have

def loc := quotient \$ localization.setoid α S


and the namespace is called localization. Should we change this so that both are called loc or both are called localization?

#### Johan Commelin (Mar 05 2019 at 08:58):

I don't think it will matter too much for projection notation (in this particular use case).

#### Patrick Massot (Mar 05 2019 at 08:59):

I vote for localization. You can still define an abbreviation (or even a local notation) in files where this is used a lot

Last updated: May 12 2021 at 08:14 UTC