Commit 2024-02-12 12:14 f9d86759

feat(NumberTheory/ArithmeticFunction): add separate scopes for notations (and a lemma) (#10403) This adds individual scopes ArithmeticFunction.zeta, ..., ArithmeticFunction.Omega, ArithmeticFunction.Moebius, ArithmeticFunction.vonMangoldt for the notations ζ, σ, ω, Ω and μ, Λ. This makes it possible to access a selected subset of these instead of either none or all of them. We also add the lemma ArithmeticFunction.pmul_assoc. See here and here on Zulip.