Topic: doc-gen searches docstrings!
Anne Baanen (Jul 21 2022 at 16:05):
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 (Jul 21 2022 at 16:08):
Last updated: Aug 03 2023 at 10:10 UTC