squarefree, is_prime_pow, and factorization

Stream: general

[Stuart Presnell]

I was trying to generalise a lemma in data/nat/factorization (#14576) to use squarefree rather than prime. But in doing so I've found that algebra/squarefree imports number_theory/divisors and algebra/is_prime_pow, and the latter imports data/nat/factorization. So I can't add an import of squarefree to factorization without generating an import cycle.

Does this arrangement of imports seem right? The definition of squarefree holds in an arbitrary monoid, so it seems strange to have this later in the import hierarchy than data/nat/factorization.

Would it make sense to split out the nat specific parts of algebra/squarefree (about 500 of the file's 720 lines) into a new data/nat/squarefree? Or is there a logic to the current sequence of dependencies that I'm not seeing?

[Eric Rodriguez]

This seems fairly sensible to me!

[Bhavik Mehta]

I agree it's weird that algebra/squarefree imports data/nat/factorization, but I think part of the issue is that algebra/is_prime_pow does too - perhaps the nat results from there could be split out as well?

[Stuart Presnell]

#14577

[Stuart Presnell]

#14598

[Stuart Presnell]

I’ve split is_prime_power in the simplest way possible, just taking out the import of factorization and then iteratively moving across anything that breaks.

[Yaël Dillies]

Could you move data.nat.factorization to data.nat.factorization.basic and the new file to data.nat.factorization.prime_pow?