User names are not rendered in notifications of comment pings

[cellio]

https://meta.codidact.com/posts/286425

In a live comment, a pinged user is rendered as @username. In a comment notification, however, that ping shows up as @number. It would be nice if the notification could show the actual user name, particularly if a comment refers to someone other than the recipient of the notification.

I would have marked this as low priority (nice to have but no rush), but that post currently has 12 upvotes, so I'll leave it at medium on the theory that it's bugging a bunch of people.