mathlib

80ae52a9 - refactor(data/nat/factorization): Change definition of `factorization` to be computable (#12301)

refactor(data/nat/factorization): Change definition of `factorization` to be computable (#12301) This PR changes the definition of `data.nat.factorization` to not depend on `multiset.to_finsupp` and instead to depend on `padic_val_nat`. This sidesteps the computability issues with finsupp discussed in [this thread](https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.60ite.60.20with.20multiple.20decidable.20instances/near/272409877). To deal with the changed imports this PR also moves some material from `number_theory/padics/padic_val` and `ring_theory/multiplicity` into `data/nat/factorization/basic`. Co-authored-by: Stuart Presnell <stuart.presnell@gmail.com> Co-authored-by: Stuart Presnell <stuart.presnell@gmail.com>