localization.of

Stream: maths

[Johan Commelin]

At some point there was some discussion about this (maybe on Github). Anyway, currently we have in ring_theory/localization.lean
https://github.com/leanprover-community/mathlib/blob/master/src/ring_theory/localization.lean#L71
a line reading

def of (r : α) (s : S) : loc α S := ⟦(r, s)⟧

But we don't have an explicit name for the ring morphism from R to localization R S. Currently the file uses \lam x, of x 1 which is not very user friendly. I would expect that this ring morphism would be called localization.of. What are others opinions on this? Would it be OK to rename the current of to mk?

[Chris Hughes]

I would rename of to mk

[Johan Commelin]

Do you want a PR?

[Johan Commelin]

@Kenny Lau What is your opinion?

[Kenny Lau]

just PR what you want :}

[Kevin Buzzard]

I independently ran into this the other day. I definitely vote for a name other than of x 1.

[Johan Commelin]

On the other hand, should S be an explicit parameter of of? (S is the submonoid at which we localise.)

[Chris Hughes]

It's inferred by the type of s

[Johan Commelin]

s = 1

[Johan Commelin]

For mk I agree