[Merged by Bors] - chore: reduce proof dependencies for Nat.factors_count_eq

[Ruben-VandeVelde]

This is a bit longer, partially duplicating the argument from UniqueFactorizationMonoid.multiplicity_eq_count_normalizedFactors, but it means we no longer need to depend on RingTheory.Int.Basic at this point.

The other added lemmas seem useful regardless.

---

[MichaelStollBayreuth]

LGTM

[eric-wieser]

I don't understand why depending on UFDs for nat factorization is a bad thing; why make the generalization if we're then going to re-derive the results without it anyway?

Are UFDs an overly-heavy import? Can we reduce that dependency tree instead?

[Ruben-VandeVelde]

Not sure why I wrote UFDs there - it's more than just the definition, but the instance for Nat is in RingTheory.Int.Basic, which pulls in a bunch of theory besides - PIDs, Euclidean domains, ideals... It's a trade-off, but I think I lean towards this change being a net positive. Happy to defer to the maintainers, though.

For UFDs in particular, we can lighten a bit by moving IsNoetherianRing.wfDvdMonoid and Ideal.IsPrime.exists_mem_prime_of_ne_bot. This might be a good idea in any case.

[semorrison]

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style