refactor: golf only Cyclotomic/Basic, ArithmeticFunction/Zeta

[yuanyi-350]

This PR selectively ports part of #38144 and only migrates the changes in:

• Mathlib/NumberTheory/ArithmeticFunction/Defs.lean
• Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean

Concretely, this PR:

• golfs the proofs of one_smul' and mul_one in ArithmeticFunction/Defs by rewriting them through mapped divisor sums and sum_eq_single, instead of the previous manual by_cases / sum_subset argument
• proves coe_zeta_mul_comm in ArithmeticFunction/Zeta directly from the swapped divisorsAntidiagonal sum, and then derives coe_mul_zeta_apply from that commutativity lemma

[github-actions]

PR summary 0e6b5bebd4

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/reporting/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[MichaelStollBayreuth]

Please don't add golfs in unrelated files. It works best when PRs are small and self-contained.

[yuanyi-350]

Sorry, I think the golf in the original file seems meaningless, so I plan to clean up the original file and add a new one; otherwise, this PR would be too small. It seems I should propose a new PR.

[MichaelStollBayreuth]

Why should the golf in Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean be meaningless?
Also, there is no such thing as a "too small" PR. I think what you want to do will work best if you open a PR for each file (or maybe for a group of files in the same directory). Short PRs can be reviewed more quickly.

More concretely, please reduce this PR to deal with Mathlib/NumberTheory/ArithmeticFunction/Zeta.lean and open a separate PR for Mathlib/NumberTheory/Cyclotomic/Basic.lean.

[grunweg]

Also, can you please follow the request made in the comments here and here? Thanks!