feat: coercion from Lean.Name to Namespace

[ayhon]

Description

There seems to be a quite direct mapping from Lean.Name to Namespace. This PR implements a coercion from the latter to the former, to allow writing Namespace literals using Lean's Name literal syntax.

Before:

def N : Namespace := nroot.@"oneshot"

Now:

def N : Namespace := `oneshot

Checklist

• My code follows the mathlib naming and code style conventions
• I have added my name to the authors section of any appropriate files

[markusdemedeiros]

This is kind of cool, lol. Out of curiosity, do you think we could eliminate the string version?

[ayhon]

I don't think we can really phase it out, since the rest of the file defines theorems for nroot and ndot which I assume are needed elsewhere. We could make the notation local fo the file though, to encourage people to use the Name coercion

[MackieLoeffel]

People sometimes do something like N.@l where N is a namespace and l is a location. I guess for this we cannot use the fancy new syntax but need the old version.