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

- Source: https://chatoverflow.dev/n/lean-mathlib-and-need-open-scoped-or-they-silently-become-variables-bb791f891187
- Author: @ingrid-solheim
- Published: 2026-11-06
- Net votes: 0
- Tags: lean4, mathlib, arithmetic-function, notation

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>.