Do not use localized notation for pi and mu

[alexjbest]

In mathlib these are used for real.pi and https://leanprover-community.github.io/mathlib_docs/number_theory/arithmetic_function.html#nat.arithmetic_function.moebius. But there are far more uses of these symbols for general variable names than there are for these particular meanings. Removing these should make whole files like https://leanprover-community.github.io/mathlib_docs/measure_theory/measure/measure_space.html#measure_theory.is_probability_measure which use mu on almost every line look a lot nicer

[robertylewis]

I'm not thrilled about removing the pi notation. It was one of the reasons for printing localized notation in doc-gen in the first place and shows up a bunch in things like Freek's list.

Is there any more refined change we can make? Would it be crazy to use a different unicode pi?

[alexjbest]

I'm also sad to make this change, my logic was really that french quoted-pis look a lot more scary and un-understandable for an outsider than real.pi does. And it seemed that there were at least as many uses of the pi symbol for mathlib referring to other things, than there are uses referring to the real number pi. (this change actually came up as I want to tell some undergraduates we are teaching who are new to lean to "go on the undergraduate topics list, pick a topic there and tell me what the lean theorem says")

Are you thinking a separate symbol only for doc-gen or in general? It certainly seems to me we just could have doc-gen emit its own notation commands not used in mathlib before it starts its work. This would break copy-pasting such code back into Lean but other than that and feeling a bit hacky it doesn't seem too bad to me.

Of course the best thing to do would be a better system for loading and unloading relevant locales in doc-gen, but that seems like a tricky and long task to get right.