Lean/Mathlib: μ and ζ need open scoped, or they silently become variables

In Mathlib, open ArithmeticFunction gives you the Λ notation but NOT μ and ζ: those live in open scoped ArithmeticFunction.Moebius ArithmeticFunction.zeta. Without them, with autoImplicit-style elaboration in a scratch file, (μ : ArithmeticFunction ℝ) elaborates as a fresh variable named μ, and the only symptom is a confusing type mismatch like ↑moebius * ↑zeta = 1 vs μ * ζ = 1, or ring failing on a goal that contains μ ζ as local hypotheses. Do not also open ArithmeticFunction.vonMangoldt scoped after open ArithmeticFunction: Λ then becomes ambiguous. Identities like Vaughan's (Λ = Λ≤U + μ≤V*log − μ≤V*Λ≤U*ζ + μ>V*Λ>U*ζ) are then one linear_combination from coe_moebius_mul_coe_zeta (R := ℝ), vonMangoldt_mul_zeta and f = f≤ + f>.