[Merged by Bors] - chore(NumberTheory/ArithmeticFunction): remove Nat. part from ArithmeticFunction namespace

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -37,7 +37,7 @@ theorem odd_mersenne_succ (k : ℕ) : ¬2 ∣ mersenne (k + 1) := by
 
 namespace Nat
 
-open Nat.ArithmeticFunction Finset
+open ArithmeticFunction Finset
 
 theorem sigma_two_pow_eq_mersenne_succ (k : ℕ) : σ 1 (2 ^ k) = mersenne (k + 1) := by
   simp_rw [sigma_one_apply, mersenne, show 2 = 1 + 1 from rfl, ← geom_sum_mul_add 1 (k + 1)]

Mathlib/NumberTheory/EulerProduct/Basic.lean

@@ -15,9 +15,9 @@ The main result in this file is `EulerProduct.eulerProduct`, which says that
 if `f : ℕ → R` is norm-summable, where `R` is a complete normed commutative ring and `f` is
 multiplicative on coprime arguments with `f 0 = 0`, then
 `∏ p in primesBelow N, ∑' e : ℕ, f (p^e)` tends to `∑' n, f n` as `N` tends to infinity.
-`Nat.ArithmeticFunction.IsMultiplicative.eulerProduct` is a version of
+`ArithmeticFunction.IsMultiplicative.eulerProduct` is a version of
 `EulerProduct.eulerProduct` for multiplicative arithmetic functions in the sense of
-`Nat.ArithmeticFunction.IsMultiplicative`.
+`ArithmeticFunction.IsMultiplicative`.
 
 There is also a version `EulerProduct.eulerProduct_completely_multiplicative`, which states that
 `∏ p in primesBelow N, (1 - f p)⁻¹` tends to `∑' n, f n` as `N` tends to infinity,
@@ -132,7 +132,7 @@ complete normed commutative ring `R`: if `‖f ·‖` is summable, then
 Since there are no infinite products yet in Mathlib, we state it in the form of
 convergence of finite partial products. -/
 -- TODO: Change to use `∏'` once infinite products are in Mathlib
-nonrec theorem _root_.Nat.ArithmeticFunction.IsMultiplicative.eulerProduct
+nonrec theorem _root_.ArithmeticFunction.IsMultiplicative.eulerProduct
     {f : ArithmeticFunction R} (hf : f.IsMultiplicative) (hsum : Summable (‖f ·‖)) :
     Tendsto (fun n : ℕ ↦ ∏ p in primesBelow n, ∑' e, f (p ^ e)) atTop (𝓝 (∑' n, f n)) :=
   eulerProduct hf.1 hf.2 hsum f.map_zero

Mathlib/NumberTheory/LSeries/Basic.lean

@@ -16,15 +16,15 @@ import Mathlib.Topology.Algebra.InfiniteSum.Basic
 Given an arithmetic function, we define the corresponding L-series.
 
 ## Main Definitions
- * `Nat.ArithmeticFunction.LSeries` is the `LSeries` with a given arithmetic function as its
+ * `ArithmeticFunction.LSeries` is the `LSeries` with a given arithmetic function as its
   coefficients. This is not the analytic continuation, just the infinite series.
- * `Nat.ArithmeticFunction.LSeriesSummable` indicates that the `LSeries`
+ * `ArithmeticFunction.LSeriesSummable` indicates that the `LSeries`
   converges at a given point.
 
 ## Main Results
- * `Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real`: the `LSeries` of a bounded
+ * `ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real`: the `LSeries` of a bounded
   arithmetic function converges when `1 < z.re`.
- * `Nat.ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re`: the `LSeries` of `ζ`
+ * `ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re`: the `LSeries` of `ζ`
   (whose analytic continuation is the Riemann ζ) converges iff `1 < z.re`.
 
 -/
@@ -34,29 +34,29 @@ noncomputable section
 
 open scoped BigOperators
 
-namespace Nat
-
 namespace ArithmeticFunction
 
+open Nat
+
 /-- The L-series of an `ArithmeticFunction`. -/
 def LSeries (f : ArithmeticFunction ℂ) (z : ℂ) : ℂ :=
   ∑' n, f n / n ^ z
-#align nat.arithmetic_function.l_series Nat.ArithmeticFunction.LSeries
+#align nat.arithmetic_function.l_series ArithmeticFunction.LSeries
 
 /-- `f.LSeriesSummable z` indicates that the L-series of `f` converges at `z`. -/
 def LSeriesSummable (f : ArithmeticFunction ℂ) (z : ℂ) : Prop :=
   Summable fun n => f n / n ^ z
-#align nat.arithmetic_function.l_series_summable Nat.ArithmeticFunction.LSeriesSummable
+#align nat.arithmetic_function.l_series_summable ArithmeticFunction.LSeriesSummable
 
 theorem LSeries_eq_zero_of_not_LSeriesSummable (f : ArithmeticFunction ℂ) (z : ℂ) :
     ¬f.LSeriesSummable z → f.LSeries z = 0 :=
   tsum_eq_zero_of_not_summable
-#align nat.arithmetic_function.l_series_eq_zero_of_not_l_series_summable Nat.ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable
+#align nat.arithmetic_function.l_series_eq_zero_of_not_l_series_summable ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable
 
 @[simp]
 theorem LSeriesSummable_zero {z : ℂ} : LSeriesSummable 0 z := by
   simp [LSeriesSummable, summable_zero]
-#align nat.arithmetic_function.l_series_summable_zero Nat.ArithmeticFunction.LSeriesSummable_zero
+#align nat.arithmetic_function.l_series_summable_zero ArithmeticFunction.LSeriesSummable_zero
 
 theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ArithmeticFunction ℂ} {m : ℝ}
     (h : ∀ n : ℕ, Complex.abs (f n) ≤ m) {z : ℝ} (hz : 1 < z) : f.LSeriesSummable z := by
@@ -75,7 +75,7 @@ theorem LSeriesSummable_of_bounded_of_one_lt_real {f : ArithmeticFunction ℂ} {
     simp only [map_div₀, Complex.norm_eq_abs]
     apply div_le_div hm (h _) (Real.rpow_pos_of_pos (Nat.cast_pos.2 n.succ_pos) _) (le_of_eq _)
     rw [Complex.abs_cpow_real, Complex.abs_natCast]
-#align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_real Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real
+#align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_real ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real
 
 theorem LSeriesSummable_iff_of_re_eq_re {f : ArithmeticFunction ℂ} {w z : ℂ} (h : w.re = z.re) :
     f.LSeriesSummable w ↔ f.LSeriesSummable z := by
@@ -93,14 +93,14 @@ theorem LSeriesSummable_iff_of_re_eq_re {f : ArithmeticFunction ℂ} {w z : ℂ}
   right
   rw [Complex.log_im, ← Complex.ofReal_nat_cast]
   exact Complex.arg_ofReal_of_nonneg (le_of_lt (cast_pos.2 n.succ_pos))
-#align nat.arithmetic_function.l_series_summable_iff_of_re_eq_re Nat.ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re
+#align nat.arithmetic_function.l_series_summable_iff_of_re_eq_re ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re
 
 theorem LSeriesSummable_of_bounded_of_one_lt_re {f : ArithmeticFunction ℂ} {m : ℝ}
     (h : ∀ n : ℕ, Complex.abs (f n) ≤ m) {z : ℂ} (hz : 1 < z.re) : f.LSeriesSummable z := by
   rw [← LSeriesSummable_iff_of_re_eq_re (Complex.ofReal_re z.re)]
   apply LSeriesSummable_of_bounded_of_one_lt_real h
   exact hz
-#align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_re Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re
+#align nat.arithmetic_function.l_series_summable_of_bounded_of_one_lt_re ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re
 
 open scoped ArithmeticFunction
 
@@ -118,7 +118,7 @@ theorem zeta_LSeriesSummable_iff_one_lt_re {z : ℂ} : LSeriesSummable ζ z ↔
     simp only [cast_zero, natCoe_apply, zeta_apply, succ_ne_zero, if_false, cast_succ, one_div,
       Complex.norm_eq_abs, map_inv₀, Complex.abs_cpow_real, inv_inj, zero_add]
     rw [← cast_one, ← cast_add, Complex.abs_natCast, cast_add, cast_one]
-#align nat.arithmetic_function.zeta_l_series_summable_iff_one_lt_re Nat.ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re
+#align nat.arithmetic_function.zeta_l_series_summable_iff_one_lt_re ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re
 
 @[simp]
 theorem LSeries_add {f g : ArithmeticFunction ℂ} {z : ℂ} (hf : f.LSeriesSummable z)
@@ -127,8 +127,6 @@ theorem LSeries_add {f g : ArithmeticFunction ℂ} {z : ℂ} (hf : f.LSeriesSumm
   rw [← tsum_add hf hg]
   apply congr rfl (funext fun n => _)
   simp [_root_.add_div]
-#align nat.arithmetic_function.l_series_add Nat.ArithmeticFunction.LSeries_add
+#align nat.arithmetic_function.l_series_add ArithmeticFunction.LSeries_add
 
 end ArithmeticFunction
-
-end Nat

Mathlib/NumberTheory/VonMangoldt.lean

@@ -19,39 +19,36 @@ In this file we define the von Mangoldt function: the function on natural number
 
 The main definition for this file is
 
-- `Nat.ArithmeticFunction.vonMangoldt`: The von Mangoldt function `Λ`.
+- `ArithmeticFunction.vonMangoldt`: The von Mangoldt function `Λ`.
 
 We then prove the classical summation property of the von Mangoldt function in
-`Nat.ArithmeticFunction.vonMangoldt_sum`, that `∑ i in n.divisors, Λ i = Real.log n`, and use this
+`ArithmeticFunction.vonMangoldt_sum`, that `∑ i in n.divisors, Λ i = Real.log n`, and use this
 to deduce alternative expressions for the von Mangoldt function via Möbius inversion, see
-`Nat.ArithmeticFunction.sum_moebius_mul_log_eq`.
+`ArithmeticFunction.sum_moebius_mul_log_eq`.
 
 ## Notation
 
 We use the standard notation `Λ` to represent the von Mangoldt function.
 
 -/
 
-
-namespace Nat
-
 namespace ArithmeticFunction
 
-open Finset
+open Finset Nat
 
 open scoped ArithmeticFunction
 
-/-- `log` as an arithmetic function `ℕ → ℝ`. Note this is in the `Nat.ArithmeticFunction`
+/-- `log` as an arithmetic function `ℕ → ℝ`. Note this is in the `ArithmeticFunction`
 namespace to indicate that it is bundled as an `ArithmeticFunction` rather than being the usual
 real logarithm. -/
 noncomputable def log : ArithmeticFunction ℝ :=
   ⟨fun n => Real.log n, by simp⟩
-#align nat.arithmetic_function.log Nat.ArithmeticFunction.log
+#align nat.arithmetic_function.log ArithmeticFunction.log
 
 @[simp]
 theorem log_apply {n : ℕ} : log n = Real.log n :=
   rfl
-#align nat.arithmetic_function.log_apply Nat.ArithmeticFunction.log_apply
+#align nat.arithmetic_function.log_apply ArithmeticFunction.log_apply
 
 /--
 The `vonMangoldt` function is the function on natural numbers that returns `log p` if the input can
@@ -63,81 +60,81 @@ In the `ArithmeticFunction` locale, we have the notation `Λ` for this function.
 -/
 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 Nat.ArithmeticFunction.vonMangoldt
+#align nat.arithmetic_function.von_mangoldt ArithmeticFunction.vonMangoldt
 
-@[inherit_doc] scoped[Nat.ArithmeticFunction] notation "Λ" => Nat.ArithmeticFunction.vonMangoldt
+@[inherit_doc] scoped[ArithmeticFunction] 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 Nat.ArithmeticFunction.vonMangoldt_apply
+#align nat.arithmetic_function.von_mangoldt_apply ArithmeticFunction.vonMangoldt_apply
 
 @[simp]
 theorem vonMangoldt_apply_one : Λ 1 = 0 := by simp [vonMangoldt_apply]
-#align nat.arithmetic_function.von_mangoldt_apply_one Nat.ArithmeticFunction.vonMangoldt_apply_one
+#align nat.arithmetic_function.von_mangoldt_apply_one ArithmeticFunction.vonMangoldt_apply_one
 
 @[simp]
 theorem vonMangoldt_nonneg {n : ℕ} : 0 ≤ Λ n := by
   rw [vonMangoldt_apply]
   split_ifs
   · exact Real.log_nonneg (one_le_cast.2 (Nat.minFac_pos n))
   rfl
-#align nat.arithmetic_function.von_mangoldt_nonneg Nat.ArithmeticFunction.vonMangoldt_nonneg
+#align nat.arithmetic_function.von_mangoldt_nonneg ArithmeticFunction.vonMangoldt_nonneg
 
 theorem vonMangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) : Λ (n ^ k) = Λ n := by
   simp only [vonMangoldt_apply, isPrimePow_pow_iff hk, pow_minFac hk]
-#align nat.arithmetic_function.von_mangoldt_apply_pow Nat.ArithmeticFunction.vonMangoldt_apply_pow
+#align nat.arithmetic_function.von_mangoldt_apply_pow ArithmeticFunction.vonMangoldt_apply_pow
 
 theorem vonMangoldt_apply_prime {p : ℕ} (hp : p.Prime) : Λ p = Real.log p := by
   rw [vonMangoldt_apply, Prime.minFac_eq hp, if_pos hp.prime.isPrimePow]
-#align nat.arithmetic_function.von_mangoldt_apply_prime Nat.ArithmeticFunction.vonMangoldt_apply_prime
+#align nat.arithmetic_function.von_mangoldt_apply_prime ArithmeticFunction.vonMangoldt_apply_prime
 
 theorem vonMangoldt_ne_zero_iff {n : ℕ} : Λ n ≠ 0 ↔ IsPrimePow n := by
   rcases eq_or_ne n 1 with (rfl | hn); · simp [not_isPrimePow_one]
   exact (Real.log_pos (one_lt_cast.2 (minFac_prime hn).one_lt)).ne'.ite_ne_right_iff
-#align nat.arithmetic_function.von_mangoldt_ne_zero_iff Nat.ArithmeticFunction.vonMangoldt_ne_zero_iff
+#align nat.arithmetic_function.von_mangoldt_ne_zero_iff ArithmeticFunction.vonMangoldt_ne_zero_iff
 
 theorem vonMangoldt_pos_iff {n : ℕ} : 0 < Λ n ↔ IsPrimePow n :=
   vonMangoldt_nonneg.lt_iff_ne.trans (ne_comm.trans vonMangoldt_ne_zero_iff)
-#align nat.arithmetic_function.von_mangoldt_pos_iff Nat.ArithmeticFunction.vonMangoldt_pos_iff
+#align nat.arithmetic_function.von_mangoldt_pos_iff ArithmeticFunction.vonMangoldt_pos_iff
 
 theorem vonMangoldt_eq_zero_iff {n : ℕ} : Λ n = 0 ↔ ¬IsPrimePow n :=
   vonMangoldt_ne_zero_iff.not_right
-#align nat.arithmetic_function.von_mangoldt_eq_zero_iff Nat.ArithmeticFunction.vonMangoldt_eq_zero_iff
+#align nat.arithmetic_function.von_mangoldt_eq_zero_iff ArithmeticFunction.vonMangoldt_eq_zero_iff
 
 open scoped BigOperators
 
 theorem vonMangoldt_sum {n : ℕ} : ∑ i in n.divisors, Λ i = Real.log n := by
   refine' recOnPrimeCoprime _ _ _ n
   · simp
   · intro p k hp
-    rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', pow_zero,
+    rw [sum_divisors_prime_pow hp, cast_pow, Real.log_pow, Finset.sum_range_succ', Nat.pow_zero,
       vonMangoldt_apply_one]
     simp [vonMangoldt_apply_pow (Nat.succ_ne_zero _), vonMangoldt_apply_prime hp]
   intro a b ha' hb' hab ha hb
   simp only [vonMangoldt_apply, ← sum_filter] at ha hb ⊢
   rw [mul_divisors_filter_prime_pow hab, filter_union,
     sum_union (disjoint_divisors_filter_isPrimePow hab), ha, hb, Nat.cast_mul,
     Real.log_mul (cast_ne_zero.2 (pos_of_gt ha').ne') (cast_ne_zero.2 (pos_of_gt hb').ne')]
-#align nat.arithmetic_function.von_mangoldt_sum Nat.ArithmeticFunction.vonMangoldt_sum
+#align nat.arithmetic_function.von_mangoldt_sum ArithmeticFunction.vonMangoldt_sum
 
 @[simp]
 theorem vonMangoldt_mul_zeta : Λ * ζ = log := by
   ext n; rw [coe_mul_zeta_apply, vonMangoldt_sum]; rfl
-#align nat.arithmetic_function.von_mangoldt_mul_zeta Nat.ArithmeticFunction.vonMangoldt_mul_zeta
+#align nat.arithmetic_function.von_mangoldt_mul_zeta ArithmeticFunction.vonMangoldt_mul_zeta
 
 @[simp]
 theorem zeta_mul_vonMangoldt : (ζ : ArithmeticFunction ℝ) * Λ = log := by rw [mul_comm]; simp
-#align nat.arithmetic_function.zeta_mul_von_mangoldt Nat.ArithmeticFunction.zeta_mul_vonMangoldt
+#align nat.arithmetic_function.zeta_mul_von_mangoldt ArithmeticFunction.zeta_mul_vonMangoldt
 
 @[simp]
 theorem log_mul_moebius_eq_vonMangoldt : log * μ = Λ := by
   rw [← vonMangoldt_mul_zeta, mul_assoc, coe_zeta_mul_coe_moebius, mul_one]
-#align nat.arithmetic_function.log_mul_moebius_eq_von_mangoldt Nat.ArithmeticFunction.log_mul_moebius_eq_vonMangoldt
+#align nat.arithmetic_function.log_mul_moebius_eq_von_mangoldt ArithmeticFunction.log_mul_moebius_eq_vonMangoldt
 
 @[simp]
 theorem moebius_mul_log_eq_vonMangoldt : (μ : ArithmeticFunction ℝ) * log = Λ := by
   rw [mul_comm]; simp
-#align nat.arithmetic_function.moebius_mul_log_eq_von_mangoldt Nat.ArithmeticFunction.moebius_mul_log_eq_vonMangoldt
+#align nat.arithmetic_function.moebius_mul_log_eq_von_mangoldt ArithmeticFunction.moebius_mul_log_eq_vonMangoldt
 
 theorem sum_moebius_mul_log_eq {n : ℕ} : (∑ d in n.divisors, (μ d : ℝ) * log d) = -Λ n := by
   simp only [← log_mul_moebius_eq_vonMangoldt, mul_comm log, mul_apply, log_apply, intCoe_apply, ←
@@ -156,16 +153,14 @@ theorem sum_moebius_mul_log_eq {n : ℕ} : (∑ d in n.divisors, (μ d : ℝ) *
   rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self,
     moebius_mul_coe_zeta]
   rcases eq_or_ne n 1 with (hn | hn) <;> simp [hn]
-#align nat.arithmetic_function.sum_moebius_mul_log_eq Nat.ArithmeticFunction.sum_moebius_mul_log_eq
+#align nat.arithmetic_function.sum_moebius_mul_log_eq ArithmeticFunction.sum_moebius_mul_log_eq
 
 theorem vonMangoldt_le_log : ∀ {n : ℕ}, Λ n ≤ Real.log (n : ℝ)
   | 0 => by simp
   | n + 1 => by
     rw [← vonMangoldt_sum]
     exact single_le_sum (by exact fun _ _ => vonMangoldt_nonneg)
       (mem_divisors_self _ n.succ_ne_zero)
-#align nat.arithmetic_function.von_mangoldt_le_log Nat.ArithmeticFunction.vonMangoldt_le_log
+#align nat.arithmetic_function.von_mangoldt_le_log ArithmeticFunction.vonMangoldt_le_log
 
 end ArithmeticFunction
-
-end Nat

Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean

@@ -455,9 +455,9 @@ set_option linter.uppercaseLean3 false in
 
 section ArithmeticFunction
 
-open Nat.ArithmeticFunction
+open ArithmeticFunction
 
-open scoped Nat.ArithmeticFunction
+open scoped ArithmeticFunction
 
 /-- `cyclotomic n R` can be expressed as a product in a fraction field of `R[X]`
   using Möbius inversion. -/

docs/overview.yaml

@@ -130,7 +130,7 @@ General algebra:
     quadratic reciprocity: 'legendreSym.quadratic_reciprocity'
     "solutions to Pell's equation": 'Pell.pell'
     "Matiyasevič's theorem": 'Pell.matiyasevic'
-    arithmetic functions: 'Nat.ArithmeticFunction'
+    arithmetic functions: 'ArithmeticFunction'
     Bernoulli numbers: 'bernoulli'
     Chevalley-Warning theorem: 'char_dvd_card_solutions'
     "Hensel's lemma (for $\\mathbb{Z}_p$)": 'hensels_lemma'