mathlib3

a8d37c1d - feat(data/nat/factorization): Defining `factorization` (#10540)

feat(data/nat/factorization): Defining `factorization` (#10540) Defining `factorization` as a `finsupp`, as discussed in https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Prime.20factorizations and https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/Proof.20of.20Euler's.20product.20formula.20for.20totient This is the first of a series of PRs to build up the infrastructure needed for the proof of Euler's product formula for the totient function.