Commit 2022-07-20 19:03 80ae52a9
View on Github →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.
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.