feat(IK): prove the three divisor-decomposition lemmas locally

[Chessing234]

unique_divisor_decomposition, sum_divisors_mul_of_coprime and divisors_mul_injective are all sorry, each marked as upstreamed to Mathlib PR #36495. That PR is not in the pinned Mathlib (Nat.divisors has no such lemmas there today), so the three are open in the meantime and #print axioms on anything above them reports sorryAx.

The proofs are short:

• unique_divisor_decomposition — existence is exists_dvd_and_dvd_of_dvd_mul; uniqueness because the first component is forced: for any admissible pair, gcd(d, a) is that component, since the second component divides b and is therefore coprime to a.
• sum_divisors_mul_of_coprime — the divisor sum of f is the Dirichlet convolution ζ * f, and IsMultiplicative.mul says a convolution of multiplicative functions is multiplicative, so map_mul_of_coprime gives it directly.
• divisors_mul_injective — the uniqueness half of the first lemma.

I know the intent is to take these from Mathlib once the bump lands — happy to close this if you would rather wait. Swapping a local proof for the upstream lemma later is a one-line change per site, whereas the sorrys are load-bearing for everything above them today.

$ lake build PrimeNumberTheoremAnd.IwaniecKowalskiCh1
Build completed successfully (3567 jobs).        # no new warnings

$ #print axioms ArithmeticFunction.unique_divisor_decomposition
  … depends on axioms: [propext, Classical.choice, Quot.sound]
$ #print axioms ArithmeticFunction.sum_divisors_mul_of_coprime
  … depends on axioms: [propext, Classical.choice, Quot.sound]
$ #print axioms ArithmeticFunction.divisors_mul_injective
  … depends on axioms: [propext, Classical.choice, Quot.sound]

Refs #1011.