[Merged by Bors] - refactor(data/nat/factorization): Change definition of factorization to be computable

[BoltonBailey]

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.

Co-authored-by: Stuart Presnell stuart.presnell@gmail.com

---

• depends on: [Merged by Bors] - refactor(number_theory/padics/padic_norm): Switch nat and rat definitions #12454
• depends on: [Merged by Bors] - refactor(number_theory/padics/padic_norm): split file #13576
• depends on: [Merged by Bors] - feat(data/part): add get_or_else_of_dom #13588

[ericrbg]

I think if you want to do this, the right way is to make a computable multiset.to_finsupp without the add part

[BoltonBailey]

As Reid said here, the algorithm to compute nat.factors is one you would never want to use. In particular, I think that if we do this by making a computable multiset.to_finsupp, then when we call n.factorization p, we will have to completely factorize n, which will ultimately take time O(sqrt(max prime factor of n)). But this way, we are just getting the multiplicity of p in n the standard way and then checking that p is prime (which will be very fast if p is, say, 2).

[stuart-presnell]

The proofs of factorization_zero and factorization_one can change to by simpa [factorization], and the proof of support_factorization becomes by simp [factorization].

[BoltonBailey]

Thanks for the helpful comments, I'll wait to implement them until this refactor of padic_norm is done if that's all right.

[stuart-presnell]

Your most recent commit seems to be deleting the entire file src/data/part.lean. Is this an error (or am I misunderstanding)?

[BoltonBailey]

Your most recent commit seems to be deleting the entire file src/data/part.lean. Is this an error (or am I misunderstanding)?

Yes, I spun off a change to that file into a new PR, and then I hit delete, thinking it would revert my changes. Sort of my fault because I guess it did what it said it was going to do, but why there's a delete file option but not a revert file option seems strange to me. I'll add it back when I merge #13588

[Vierkantor]

Thanks!

bors d+

[bors]

✌️ BoltonBailey can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[BoltonBailey]

bors r+

[bors]

Canceled.

[BoltonBailey]

bors r-

[BoltonBailey]

Ok, trying again

[BoltonBailey]

bors r+

[bors]

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests