Docs search ignores the exported name #222
Description
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.