doc-gen searches docstrings!

Stream: general

[Anne Baanen]

I just wanted to praise whoever made it so you can search for "chinese remainder" in the mathlib-docs and have docs#ideal.quotient_inf_ring_equiv_pi_quotient pop up among the suggestions, and give a tip to whoever (like me) didn't already know this!

[Rob Lewis]

doc-gen#156 , a reimplementation of a feature from doc-gen#131