bump to nightly-2024-02-12-08

mathlib commit leanprover-community/mathlib@65a1391

Archive/Wiedijk100Theorems/PerfectNumbers.lean

@@ -39,7 +39,7 @@ theorem odd_mersenne_succ (k : ℕ) : ¬2 ∣ mersenne (k + 1) := by
 
 namespace Nat
 
-open Nat.ArithmeticFunction Finset
+open ArithmeticFunction Finset
 
 open scoped ArithmeticFunction
 

Mathbin/Data/Fintype/Parity.lean

@@ -28,11 +28,9 @@ instance IsSquare.decidablePred [Mul α] [Fintype α] [DecidableEq α] :
 
 end Fintype
 
-#print Fintype.card_fin_even /-
 /-- The cardinality of `fin (bit0 n)` is even, `fact` version.
 This `fact` is needed as an instance by `matrix.special_linear_group.has_neg`. -/
 theorem Fintype.card_fin_even {n : ℕ} : Fact (Even (Fintype.card (Fin (bit0 n)))) :=
   ⟨by rw [Fintype.card_fin]; exact even_bit0 _⟩
 #align fintype.card_fin_even Fintype.card_fin_even
--/
 

Mathbin/NumberTheory/LSeries.lean

@@ -41,37 +41,37 @@ namespace Nat
 
 namespace ArithmeticFunction
 
-#print Nat.ArithmeticFunction.LSeries /-
+#print ArithmeticFunction.LSeries /-
 /-- The L-series of an `arithmetic_function`. -/
-def LSeries (f : ArithmeticFunction ℂ) (z : ℂ) : ℂ :=
+def ArithmeticFunction.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
 -/
 
-#print Nat.ArithmeticFunction.LSeriesSummable /-
+#print ArithmeticFunction.LSeriesSummable /-
 /-- `f.l_series_summable z` indicates that the L-series of `f` converges at `z`. -/
-def LSeriesSummable (f : ArithmeticFunction ℂ) (z : ℂ) : Prop :=
+def ArithmeticFunction.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
 -/
 
-#print Nat.ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable /-
-theorem LSeries_eq_zero_of_not_LSeriesSummable (f : ArithmeticFunction ℂ) (z : ℂ) :
-    ¬f.LSeriesSummable z → f.LSeries z = 0 :=
+#print ArithmeticFunction.LSeries_eq_zero_of_not_LSeriesSummable /-
+theorem ArithmeticFunction.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
 -/
 
-#print Nat.ArithmeticFunction.LSeriesSummable_zero /-
+#print ArithmeticFunction.LSeriesSummable_zero /-
 @[simp]
-theorem LSeriesSummable_zero {z : ℂ} : LSeriesSummable 0 z := by
-  simp [l_series_summable, summable_zero]
-#align nat.arithmetic_function.l_series_summable_zero Nat.ArithmeticFunction.LSeriesSummable_zero
+theorem ArithmeticFunction.LSeriesSummable_zero {z : ℂ} : ArithmeticFunction.LSeriesSummable 0 z :=
+  by simp [l_series_summable, summable_zero]
+#align nat.arithmetic_function.l_series_summable_zero ArithmeticFunction.LSeriesSummable_zero
 -/
 
-#print Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real /-
-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 :=
+#print ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_real /-
+theorem ArithmeticFunction.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
   by_cases h0 : m = 0
   · subst h0
@@ -89,12 +89,12 @@ 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
 -/
 
-#print Nat.ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re /-
-theorem LSeriesSummable_iff_of_re_eq_re {f : ArithmeticFunction ℂ} {w z : ℂ} (h : w.re = z.re) :
-    f.LSeriesSummable w ↔ f.LSeriesSummable z :=
+#print ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re /-
+theorem ArithmeticFunction.LSeriesSummable_iff_of_re_eq_re {f : ArithmeticFunction ℂ} {w z : ℂ}
+    (h : w.re = z.re) : f.LSeriesSummable w ↔ f.LSeriesSummable z :=
   by
   suffices h :
     ∀ n : ℕ, Complex.abs (f n) / Complex.abs (↑n ^ w) = Complex.abs (f n) / Complex.abs (↑n ^ z)
@@ -110,23 +110,24 @@ 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
 -/
 
-#print Nat.ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_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 :=
+#print ArithmeticFunction.LSeriesSummable_of_bounded_of_one_lt_re /-
+theorem ArithmeticFunction.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 [← l_series_summable_iff_of_re_eq_re (Complex.ofReal_re z.re)]
   apply l_series_summable_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
 
-#print Nat.ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re /-
-theorem zeta_LSeriesSummable_iff_one_lt_re {z : ℂ} : LSeriesSummable ζ z ↔ 1 < z.re :=
+#print ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re /-
+theorem ArithmeticFunction.zeta_LSeriesSummable_iff_one_lt_re {z : ℂ} :
+    ArithmeticFunction.LSeriesSummable ζ z ↔ 1 < z.re :=
   by
   rw [← l_series_summable_iff_of_re_eq_re (Complex.ofReal_re z.re), l_series_summable, ←
     summable_norm_iff, ← Real.summable_one_div_nat_rpow, iff_iff_eq]
@@ -142,19 +143,20 @@ theorem zeta_LSeriesSummable_iff_one_lt_re {z : ℂ} : LSeriesSummable ζ z ↔
     simp only [cast_zero, nat_coe_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
 -/
 
-#print Nat.ArithmeticFunction.LSeries_add /-
+#print ArithmeticFunction.LSeries_add /-
 @[simp]
-theorem LSeries_add {f g : ArithmeticFunction ℂ} {z : ℂ} (hf : f.LSeriesSummable z)
-    (hg : g.LSeriesSummable z) : (f + g).LSeries z = f.LSeries z + g.LSeries z :=
+theorem ArithmeticFunction.LSeries_add {f g : ArithmeticFunction ℂ} {z : ℂ}
+    (hf : f.LSeriesSummable z) (hg : g.LSeriesSummable z) :
+    (f + g).LSeries z = f.LSeries z + g.LSeries z :=
   by
   simp only [l_series, add_apply]
   rw [← tsum_add hf hg]
   apply congr rfl (funext fun n => _)
   apply _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

Mathbin/NumberTheory/VonMangoldt.lean

@@ -44,23 +44,23 @@ open Finset
 
 open scoped ArithmeticFunction
 
-#print Nat.ArithmeticFunction.log /-
+#print ArithmeticFunction.log /-
 /-- `log` as an arithmetic function `ℕ → ℝ`. Note this is in the `nat.arithmetic_function`
 namespace to indicate that it is bundled as an `arithmetic_function` rather than being the usual
 real logarithm. -/
-noncomputable def log : ArithmeticFunction ℝ :=
+noncomputable def ArithmeticFunction.log : ArithmeticFunction ℝ :=
   ⟨fun n => Real.log n, by simp⟩
-#align nat.arithmetic_function.log Nat.ArithmeticFunction.log
+#align nat.arithmetic_function.log ArithmeticFunction.log
 -/
 
-#print Nat.ArithmeticFunction.log_apply /-
+#print ArithmeticFunction.log_apply /-
 @[simp]
-theorem log_apply {n : ℕ} : log n = Real.log n :=
+theorem ArithmeticFunction.log_apply {n : ℕ} : ArithmeticFunction.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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt /-
+#print ArithmeticFunction.vonMangoldt /-
 /--
 The `von_mangoldt` function is the function on natural numbers that returns `log p` if the input can
 be expressed as `p^k` for a prime `p`.
@@ -69,72 +69,74 @@ smallest prime factor.
 
 In the `arithmetic_function` locale, we have the notation `Λ` for this function.
 -/
-noncomputable def vonMangoldt : ArithmeticFunction ℝ :=
+noncomputable def ArithmeticFunction.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
 -/
 
-scoped[ArithmeticFunction] notation "Λ" => Nat.ArithmeticFunction.vonMangoldt
+scoped[ArithmeticFunction] notation "Λ" => ArithmeticFunction.vonMangoldt
 
-#print Nat.ArithmeticFunction.vonMangoldt_apply /-
-theorem vonMangoldt_apply {n : ℕ} : Λ n = if IsPrimePow n then Real.log (minFac n) else 0 :=
+#print ArithmeticFunction.vonMangoldt_apply /-
+theorem ArithmeticFunction.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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_apply_one /-
+#print ArithmeticFunction.vonMangoldt_apply_one /-
 @[simp]
-theorem vonMangoldt_apply_one : Λ 1 = 0 := by simp [von_mangoldt_apply]
-#align nat.arithmetic_function.von_mangoldt_apply_one Nat.ArithmeticFunction.vonMangoldt_apply_one
+theorem ArithmeticFunction.vonMangoldt_apply_one : Λ 1 = 0 := by simp [von_mangoldt_apply]
+#align nat.arithmetic_function.von_mangoldt_apply_one ArithmeticFunction.vonMangoldt_apply_one
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_nonneg /-
+#print ArithmeticFunction.vonMangoldt_nonneg /-
 @[simp]
-theorem vonMangoldt_nonneg {n : ℕ} : 0 ≤ Λ n :=
+theorem ArithmeticFunction.vonMangoldt_nonneg {n : ℕ} : 0 ≤ Λ n :=
   by
   rw [von_mangoldt_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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_apply_pow /-
-theorem vonMangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) : Λ (n ^ k) = Λ n := by
+#print ArithmeticFunction.vonMangoldt_apply_pow /-
+theorem ArithmeticFunction.vonMangoldt_apply_pow {n k : ℕ} (hk : k ≠ 0) : Λ (n ^ k) = Λ n := by
   simp only [von_mangoldt_apply, isPrimePow_pow_iff hk, pow_min_fac 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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_apply_prime /-
-theorem vonMangoldt_apply_prime {p : ℕ} (hp : p.Prime) : Λ p = Real.log p := by
+#print ArithmeticFunction.vonMangoldt_apply_prime /-
+theorem ArithmeticFunction.vonMangoldt_apply_prime {p : ℕ} (hp : p.Prime) : Λ p = Real.log p := by
   rw [von_mangoldt_apply, prime.min_fac_eq hp, if_pos hp.prime.is_prime_pow]
-#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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_ne_zero_iff /-
-theorem vonMangoldt_ne_zero_iff {n : ℕ} : Λ n ≠ 0 ↔ IsPrimePow n :=
+#print ArithmeticFunction.vonMangoldt_ne_zero_iff /-
+theorem ArithmeticFunction.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 (min_fac_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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_pos_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
+#print ArithmeticFunction.vonMangoldt_pos_iff /-
+theorem ArithmeticFunction.vonMangoldt_pos_iff {n : ℕ} : 0 < Λ n ↔ IsPrimePow n :=
+  ArithmeticFunction.vonMangoldt_nonneg.lt_iff_ne.trans
+    (ne_comm.trans ArithmeticFunction.vonMangoldt_ne_zero_iff)
+#align nat.arithmetic_function.von_mangoldt_pos_iff ArithmeticFunction.vonMangoldt_pos_iff
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_eq_zero_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
+#print ArithmeticFunction.vonMangoldt_eq_zero_iff /-
+theorem ArithmeticFunction.vonMangoldt_eq_zero_iff {n : ℕ} : Λ n = 0 ↔ ¬IsPrimePow n :=
+  ArithmeticFunction.vonMangoldt_ne_zero_iff.not_right
+#align nat.arithmetic_function.von_mangoldt_eq_zero_iff ArithmeticFunction.vonMangoldt_eq_zero_iff
 -/
 
 open scoped BigOperators
 
-#print Nat.ArithmeticFunction.vonMangoldt_sum /-
-theorem vonMangoldt_sum {n : ℕ} : ∑ i in n.divisors, Λ i = Real.log n :=
+#print ArithmeticFunction.vonMangoldt_sum /-
+theorem ArithmeticFunction.vonMangoldt_sum {n : ℕ} : ∑ i in n.divisors, Λ i = Real.log n :=
   by
   refine' rec_on_prime_coprime _ _ _ n
   · simp
@@ -147,38 +149,40 @@ theorem vonMangoldt_sum {n : ℕ} : ∑ i in n.divisors, Λ i = Real.log n :=
   rw [mul_divisors_filter_prime_pow hab, filter_union,
     sum_union (disjoint_divisors_filter_prime_pow 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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_mul_zeta /-
+#print ArithmeticFunction.vonMangoldt_mul_zeta /-
 @[simp]
-theorem vonMangoldt_mul_zeta : Λ * ζ = log := by ext n; rw [coe_mul_zeta_apply, von_mangoldt_sum];
-  rfl
-#align nat.arithmetic_function.von_mangoldt_mul_zeta Nat.ArithmeticFunction.vonMangoldt_mul_zeta
+theorem ArithmeticFunction.vonMangoldt_mul_zeta : Λ * ζ = ArithmeticFunction.log := by ext n;
+  rw [coe_mul_zeta_apply, von_mangoldt_sum]; rfl
+#align nat.arithmetic_function.von_mangoldt_mul_zeta ArithmeticFunction.vonMangoldt_mul_zeta
 -/
 
-#print Nat.ArithmeticFunction.zeta_mul_vonMangoldt /-
+#print ArithmeticFunction.zeta_mul_vonMangoldt /-
 @[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
+theorem ArithmeticFunction.zeta_mul_vonMangoldt :
+    (ζ : ArithmeticFunction ℝ) * Λ = ArithmeticFunction.log := by rw [mul_comm]; simp
+#align nat.arithmetic_function.zeta_mul_von_mangoldt ArithmeticFunction.zeta_mul_vonMangoldt
 -/
 
-#print Nat.ArithmeticFunction.log_mul_moebius_eq_vonMangoldt /-
+#print ArithmeticFunction.log_mul_moebius_eq_vonMangoldt /-
 @[simp]
-theorem log_mul_moebius_eq_vonMangoldt : log * μ = Λ := by
+theorem ArithmeticFunction.log_mul_moebius_eq_vonMangoldt : ArithmeticFunction.log * μ = Λ := by
   rw [← von_mangoldt_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
 -/
 
-#print Nat.ArithmeticFunction.moebius_mul_log_eq_vonMangoldt /-
+#print ArithmeticFunction.moebius_mul_log_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
+theorem ArithmeticFunction.moebius_mul_log_eq_vonMangoldt :
+    (μ : ArithmeticFunction ℝ) * ArithmeticFunction.log = Λ := by rw [mul_comm]; simp
+#align nat.arithmetic_function.moebius_mul_log_eq_von_mangoldt ArithmeticFunction.moebius_mul_log_eq_vonMangoldt
 -/
 
-#print Nat.ArithmeticFunction.sum_moebius_mul_log_eq /-
-theorem sum_moebius_mul_log_eq {n : ℕ} : ∑ d in n.divisors, (μ d : ℝ) * log d = -Λ n :=
+#print ArithmeticFunction.sum_moebius_mul_log_eq /-
+theorem ArithmeticFunction.sum_moebius_mul_log_eq {n : ℕ} :
+    ∑ d in n.divisors, (μ d : ℝ) * ArithmeticFunction.log d = -Λ n :=
   by
   simp only [← log_mul_moebius_eq_von_mangoldt, mul_comm log, mul_apply, log_apply, int_coe_apply, ←
     Finset.sum_neg_distrib, neg_mul_eq_mul_neg]
@@ -198,16 +202,16 @@ theorem sum_moebius_mul_log_eq {n : ℕ} : ∑ d in n.divisors, (μ d : ℝ) * l
   rw [this, sum_sub_distrib, ← sum_mul, ← Int.cast_sum, ← coe_mul_zeta_apply, eq_comm, sub_eq_self,
     moebius_mul_coe_zeta, mul_eq_zero, Int.cast_eq_zero]
   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
 -/
 
-#print Nat.ArithmeticFunction.vonMangoldt_le_log /-
-theorem vonMangoldt_le_log : ∀ {n : ℕ}, Λ n ≤ Real.log (n : ℝ)
+#print ArithmeticFunction.vonMangoldt_le_log /-
+theorem ArithmeticFunction.vonMangoldt_le_log : ∀ {n : ℕ}, Λ n ≤ Real.log (n : ℝ)
   | 0 => by simp
   | n + 1 => by
     rw [← von_mangoldt_sum]
     exact single_le_sum (fun _ _ => von_mangoldt_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

Mathbin/RingTheory/Polynomial/Cyclotomic/Basic.lean

@@ -562,7 +562,7 @@ theorem X_pow_sub_one_mul_cyclotomic_dvd_X_pow_sub_one_of_dvd (R) [CommRing R] {
 
 section ArithmeticFunction
 
-open Nat.ArithmeticFunction
+open ArithmeticFunction
 
 open scoped ArithmeticFunction