localization

Stream: maths

[Johan Commelin]

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]

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

[Patrick Massot]

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