I think you should rebase this on top of #184's commits, so it is easier to review what changed and ensure that modifications from that PR are reflected here (which does seem to be the case)

The original Mathlib alias had a comment to add an alias attribute. I'm not sure what that attribute was intended to do other than "I'm an alias of". I think even that basic functionality makes some sense but is it needed?

The attribute was intended to be usable so that third party code could programmatically determine that a declaration is an alias of another.

Should that be implemented as an attribute or as an environment extension? I'm thinking the latter since I don't see much need for @[alias ...].

Does it support protected?

Yes, it supports all modifiers and attributes the same way as def and theorem do!

Should that be implemented as an attribute or as an environment extension? I'm thinking the latter since I don't see much need for @[alias ...].

At some point I wrote a linter for duplicate lemmas and the attribute was useful as a way of skipping intentional duplicates. The interaction with to_additive was a little subtle here and it was important for that application that to_additive could copy the alias attribute to an additive version of an existing alias.

That makes sense. I think the aliasExt environment extension would work fine for that. I added a small convenience API.