chore(Nat): Nat factorization multiplicity

[Kevew]

Ported lemmas from Data/Nat/Multiplicity to into a new file called Data/Nat/Factorization/Multiplicity, re-written in terms of factorization.

Also, I'm new to this so is it fine to have a lemma copied over from another file? Like, I copied over

@[simp]
theorem Prime.factorization_self {p : ℕ} (hp : Prime p) : p.factorization p = 1 := by simp [hp]

from Dat/Nat/Factorization/Basic.

---

[github-actions]

PR summary cddbb691c5

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference
Mathlib.Data.Nat.Factorization.Multiplicity (new file)	872

---

Declarations diff

+ factorization_choose
+ factorization_choose'
+ factorization_choose_prime_pow
+ factorization_choose_prime_pow_add_factorization
+ factorization_eq_card_pow_dvd₀
+ factorization_factorial
+ factorization_factorial_le_div_pred
+ factorization_factorial_mul
+ factorization_factorial_mul_succ
+ factorization_le_factorization_choose_add
+ factorization_le_factorization_of_dvd_right
+ factorization_mul₀
+ factorization_pow_self
+ factorization_pow₀
+ factorization_prod₀
+ multiplicity_choose_aux
+ sub_one_mul_factorization_factorial

You can run this locally as follows

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

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

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

---

No changes to technical debt.

You can run this locally as

./scripts/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).

[Paul-Lez]

Note that you should be able to avoid using new lemmas such as factorization_mul₀ by using already existing API for factorization and Finsupp.

Suggested change

	have p1: n + 1 ≠ 0 := by exact Ne.symm (zero_ne_add_one n)
	apply factorization_mul₀ p1 (factorial_ne_zero n)
	_ = (n + 1).factorization p + (n !).factorization p := by
	rw [factorization_mul (zero_ne_add_one n).symm (factorial_ne_zero n), coe_add, Pi.add_apply]

One useful trick for finding such lemmas when you're writing proofs is to use the simp? tactic.

[Kevew]

Is it always preferable to use old lemmas? Like is it a convention?

I feel as though: exact factorization_mul₀ ((zero_ne_add_one n).symm) (factorial_ne_zero n)
is more readable then rw [factorization_mul (zero_ne_add_one n).symm (factorial_ne_zero n), coe_add, Pi.add_apply].

Like, factorization_mul₀ was a lemma I made so that I didn't need to use coe_add, Pi.add_apply each time I apply the old one.