From c4aa6b074e79948ab37eeb979bac37e3d8fb59b9 Mon Sep 17 00:00:00 2001 From: yuanyi-350 Date: Mon, 20 Apr 2026 17:04:25 +0800 Subject: [PATCH 1/2] refactor(NumberTheory): golf ArithmeticFunction/Zeta --- .../NumberTheory/ArithmeticFunction/Zeta.lean | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean index ab67f48c8097c5..7026d8b0cc6742 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean @@ -78,18 +78,14 @@ theorem coe_zeta_mul_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := coe_zeta_smul_apply -theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : - (f * ζ) x = ∑ i ∈ divisors x, f i := by - rw [mul_apply] - trans ∑ i ∈ divisorsAntidiagonal x, f i.1 - · refine sum_congr rfl fun i hi => ?_ - rcases mem_divisorsAntidiagonal.1 hi with ⟨rfl, h⟩ - rw [natCoe_apply, zeta_apply_ne (right_ne_zero_of_mul h), cast_one, mul_one] - · rw [← map_div_right_divisors, sum_map, Function.Embedding.coeFn_mk] - theorem coe_zeta_mul_comm [Semiring R] {f : ArithmeticFunction R} : ζ * f = f * ζ := by ext x - rw [coe_zeta_mul_apply, coe_mul_zeta_apply] + rw [mul_apply, ← map_swap_divisorsAntidiagonal, Finset.sum_map] + simp [mul_apply] + +theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : + (f * ζ) x = ∑ i ∈ divisors x, f i := by + rw [← coe_zeta_mul_comm, coe_zeta_mul_apply] theorem zeta_mul_apply {f : ArithmeticFunction ℕ} {x : ℕ} : (ζ * f) x = ∑ i ∈ divisors x, f i := by rw [← natCoe_nat ζ, coe_zeta_mul_apply] From 2455328ca522c9ca9bff28c41ee282c7ac47d6bf Mon Sep 17 00:00:00 2001 From: "Yi.Yuan" Date: Tue, 21 Apr 2026 09:11:36 +0800 Subject: [PATCH 2/2] apply suggestions --- Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean index 7026d8b0cc6742..0eac1940863b41 100644 --- a/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean +++ b/Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean @@ -74,15 +74,15 @@ theorem sum_divisorsAntidiagonal_eq_sum_divisors {M} [Semiring R] [AddCommMonoid ∑ i ∈ divisors x, f i := by simp [← coe_zeta_smul_apply (R := R)] -theorem coe_zeta_mul_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : - (ζ * f) x = ∑ i ∈ divisors x, f i := - coe_zeta_smul_apply - theorem coe_zeta_mul_comm [Semiring R] {f : ArithmeticFunction R} : ζ * f = f * ζ := by ext x rw [mul_apply, ← map_swap_divisorsAntidiagonal, Finset.sum_map] simp [mul_apply] +theorem coe_zeta_mul_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : + (ζ * f) x = ∑ i ∈ divisors x, f i := + coe_zeta_smul_apply + theorem coe_mul_zeta_apply [Semiring R] {f : ArithmeticFunction R} {x : ℕ} : (f * ζ) x = ∑ i ∈ divisors x, f i := by rw [← coe_zeta_mul_comm, coe_zeta_mul_apply]