feat(NumberTheory/ArithmeticFunction): add separate scopes for notati…

…ons (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](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Nat.2EArithmeticFunction.20--.3E.20ArithmeticFunction/near/420800408) and [here](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/How.20do.20you.20hide.20scoped.20notation/near/418117690) on Zulip.

Mathlib/NumberTheory/ArithmeticFunction.lean

@@ -21,6 +21,7 @@ functions are endowed with a multiplication, given by Dirichlet convolution, and
 to form the Dirichlet ring.
 
 ## Main Definitions
+
  * `ArithmeticFunction R` consists of functions `f : ℕ → R` such that `f 0 = 0`.
  * An arithmetic function `f` `IsMultiplicative` when `x.coprime y → f (x * y) = f x * f y`.
  * The pointwise operations `pmul` and `ppow` differ from the multiplication
@@ -34,6 +35,7 @@ to form the Dirichlet ring.
  * `μ` is the Möbius function (spelled `moebius` in code).
 
 ## Main Results
+
  * Several forms of Möbius inversion:
  * `sum_eq_iff_sum_mul_moebius_eq` for functions to a `CommRing`
  * `sum_eq_iff_sum_smul_moebius_eq` for functions to an `AddCommGroup`
@@ -47,14 +49,21 @@ to form the Dirichlet ring.
  * `prod_eq_iff_prod_pow_moebius_eq_on_of_nonzero` for functions to a `CommGroupWithZero`
 
 ## Notation
+
 All notation is localized in the namespace `ArithmeticFunction`.
 
 The arithmetic functions `ζ`, `σ`, `ω`, `Ω` and `μ` have Greek letter names.
 
+In addition, there are separate locales `ArithmeticFunction.zeta` for `ζ`,
+`ArithmeticFunction.sigma` for `σ`, `ArithmeticFunction.omega` for `ω`,
+`ArithmeticFunction.Omega` for `Ω`, and `ArithmeticFunction.Moebius` for `μ`,
+to allow for selective access to these notations.
+
 The arithmetic function $$n \mapsto \prod_{p \mid n} f(p)$$ is given custom notation
 `∏ᵖ p ∣ n, f p` when applied to `n`.
 
 ## Tags
+
 arithmetic functions, dirichlet convolution, divisors
 
 -/
@@ -418,10 +427,12 @@ def zeta : ArithmeticFunction ℕ :=
   ⟨fun x => ite (x = 0) 0 1, rfl⟩
 #align nat.arithmetic_function.zeta ArithmeticFunction.zeta
 
--- porting note: added `Nat.` to the scoped namespace
 @[inherit_doc]
 scoped[ArithmeticFunction] notation "ζ" => ArithmeticFunction.zeta
 
+@[inherit_doc]
+scoped[ArithmeticFunction.zeta] notation "ζ" => ArithmeticFunction.zeta
+
 @[simp]
 theorem zeta_apply {x : ℕ} : ζ x = if x = 0 then 0 else 1 :=
   rfl
@@ -491,6 +502,11 @@ theorem pmul_comm [CommMonoidWithZero R] (f g : ArithmeticFunction R) : f.pmul g
   simp [mul_comm]
 #align nat.arithmetic_function.pmul_comm ArithmeticFunction.pmul_comm
 
+lemma pmul_assoc [CommMonoidWithZero R] (f₁ f₂ f₃ : ArithmeticFunction R) :
+    pmul (pmul f₁ f₂) f₃ = pmul f₁ (pmul f₂ f₃) := by
+  ext
+  simp only [pmul_apply, mul_assoc]
+
 section NonAssocSemiring
 
 variable [NonAssocSemiring R]
@@ -842,10 +858,12 @@ def sigma (k : ℕ) : ArithmeticFunction ℕ :=
   ⟨fun n => ∑ d in divisors n, d ^ k, by simp⟩
 #align nat.arithmetic_function.sigma ArithmeticFunction.sigma
 
--- porting note: added `Nat.` to the scoped namespace
 @[inherit_doc]
 scoped[ArithmeticFunction] notation "σ" => ArithmeticFunction.sigma
 
+@[inherit_doc]
+scoped[ArithmeticFunction.sigma] notation "σ" => ArithmeticFunction.sigma
+
 theorem sigma_apply {k n : ℕ} : σ k n = ∑ d in divisors n, d ^ k :=
   rfl
 #align nat.arithmetic_function.sigma_apply ArithmeticFunction.sigma_apply
@@ -911,10 +929,12 @@ def cardFactors : ArithmeticFunction ℕ :=
   ⟨fun n => n.factors.length, by simp⟩
 #align nat.arithmetic_function.card_factors ArithmeticFunction.cardFactors
 
--- porting note: added `Nat.` to the scoped namespace
 @[inherit_doc]
 scoped[ArithmeticFunction] notation "Ω" => ArithmeticFunction.cardFactors
 
+@[inherit_doc]
+scoped[ArithmeticFunction.Omega] notation "Ω" => ArithmeticFunction.cardFactors
+
 theorem cardFactors_apply {n : ℕ} : Ω n = n.factors.length :=
   rfl
 #align nat.arithmetic_function.card_factors_apply ArithmeticFunction.cardFactors_apply
@@ -965,10 +985,12 @@ def cardDistinctFactors : ArithmeticFunction ℕ :=
   ⟨fun n => n.factors.dedup.length, by simp⟩
 #align nat.arithmetic_function.card_distinct_factors ArithmeticFunction.cardDistinctFactors
 
--- porting note: added `Nat.` to the scoped namespace
 @[inherit_doc]
 scoped[ArithmeticFunction] notation "ω" => ArithmeticFunction.cardDistinctFactors
 
+@[inherit_doc]
+scoped[ArithmeticFunction.omega] notation "ω" => ArithmeticFunction.cardDistinctFactors
+
 theorem cardDistinctFactors_zero : ω 0 = 0 := by simp
 #align nat.arithmetic_function.card_distinct_factors_zero ArithmeticFunction.cardDistinctFactors_zero
 
@@ -1008,10 +1030,12 @@ def moebius : ArithmeticFunction ℤ :=
   ⟨fun n => if Squarefree n then (-1) ^ cardFactors n else 0, by simp⟩
 #align nat.arithmetic_function.moebius ArithmeticFunction.moebius
 
--- porting note: added `Nat.` to the scoped namespace
 @[inherit_doc]
 scoped[ArithmeticFunction] notation "μ" => ArithmeticFunction.moebius
 
+@[inherit_doc]
+scoped[ArithmeticFunction.Moebius] notation "μ" => ArithmeticFunction.moebius
+
 @[simp]
 theorem moebius_apply_of_squarefree {n : ℕ} (h : Squarefree n) : μ n = (-1) ^ cardFactors n :=
   if_pos h

Mathlib/NumberTheory/VonMangoldt.lean

@@ -29,6 +29,8 @@ to deduce alternative expressions for the von Mangoldt function via Möbius inve
 ## Notation
 
 We use the standard notation `Λ` to represent the von Mangoldt function.
+It is accessible in the locales `ArithmeticFunction` (like the notations for other arithmetic
+functions) and also in the locale `ArithmeticFunction.vonMangoldt`.
 
 -/
 
@@ -57,13 +59,18 @@ In the case when `n` is a prime power, `min_fac` will give the appropriate prime
 smallest prime factor.
 
 In the `ArithmeticFunction` locale, we have the notation `Λ` for this function.
+This is also available in the `ArithmeticFunction.vonMangoldt` locale, allowing for selective
+access to the notation.
 -/
 noncomputable def vonMangoldt : ArithmeticFunction ℝ :=
   ⟨fun n => if IsPrimePow n then Real.log (minFac n) else 0, if_neg not_isPrimePow_zero⟩
 #align nat.arithmetic_function.von_mangoldt ArithmeticFunction.vonMangoldt
 
 @[inherit_doc] scoped[ArithmeticFunction] notation "Λ" => ArithmeticFunction.vonMangoldt
 
+@[inherit_doc] scoped[ArithmeticFunction.vonMangoldt] notation "Λ" =>
+  ArithmeticFunction.vonMangoldt
+
 theorem vonMangoldt_apply {n : ℕ} : Λ n = if IsPrimePow n then Real.log (minFac n) else 0 :=
   rfl
 #align nat.arithmetic_function.von_mangoldt_apply ArithmeticFunction.vonMangoldt_apply