mathlib can't make up its mind on whether to spell "the prime factors of `n`" as `n.factors.toFinset` or `n.factorization.support`, even though those two are defeq. This PR proposes to unify everything to a new definition `Nat.primeFactors`, and stream the existing scattered API about `n.factors.toFinset` and `n.factorization.support` to `Nat.primeFactors`. We also get to write a bit more API that didn't make sense before, eg `primeFactors_mono`.