Commit 2022-01-07 18:21 a8d37c1d

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.