Docs search ignores the exported name

[YaelDillies]

If you look for "inv_zero" in the mathlib docs, you would expect to find inv_zero as the first result. Annoyingly, you get this instead:

... because inv_zero is secretly GroupWithZero.inv_zero exported to _root_.

This is an issue because exported lemmas are usually of widespread use (else we wouldn't be exporting them in the first place), but them being exports significantly hinders their discoverability.