mathlib3

d910e835 - chore(*): ensure all open_locales work without any open namespaces (#10913)

chore(*): ensure all open_locales work without any open namespaces (#10913) Inspired by #10905 we clean up the localized notation in all locales by using the full names of declarations, this should mean that `open_locale blah` should almost never error. The cases I'm aware of where this doesn't hold still are the locales: - `witt` which hard codes the variable name `p`, if there is no `p` in context this will fail - `list.func` and `topological_space` opening `list.func` breaks the notation in `topological_space` due to ``notation as `{` m ` ↦ ` a `}` := list.func.set a as m`` in `list.func` and ``localized "notation `𝓝[≠] ` x:100 := nhds_within x {x}ᶜ" in topological_space`` - likewise for `parser` and `kronecker` due to ``localized "infix ` ⊗ₖ `:100 := matrix.kronecker_map (*)" in kronecker`` But we don't fix these in this PR. There may be others instances like this too as these errors can depend on the ordering chosen and I didn't check them all. A very basic script to check this sort of thing is at https://github.com/leanprover-community/mathlib/tree/alexjbest/check_localized