[Merged by Bors] - feat: add lemma exists_squarefree_dvd_pow_of_ne_zero

[ocfnash]

---

[adomani]

LGTM

My only comment is adding a symmetrical doc-string.

[alreadydone]

This can be strengthened to require that y divides x.

I started the DecompositionMonoid refactoring in that branch, and I think every lemma in this file can be generalized to DceompositionMonoid (and two only require CancelCommMonoidWithZero as you can see). However this new lemma can't be generalized, since (assuming DecompositionMonoid) it implies factorizability into squarefree elements, which is the subject of Proposition 3.4 in the paper. Note that DecompositionMonoid + factorizability into irreducibles would imply UFM right away.

[ocfnash]

This can be strengthened to require that y divides x.

Good point, I will add this.

I started the DecompositionMonoid refactoring in that branch ...

Great, thanks for taking this on. As an aside, I would argue that your proposed IsRelPrime should really get the label IsCoprime and what is currently called IsCoprime should either be dropped or renamed something like ExistsBezout or IsBezoutPair or something.

[alreadydone]

Having Bezout in the name is nice; IsCoprime is equivalent to IsRelPrime in Bezout rings (IsBezout), and most results in Mathlib.RingTheory.PrincipalIdealDomain can be generalized to Bezout rings (but maybe the correct approach is to replace IsCoprime by IsRelPrime and use the equivalence when necessary ...). There is IsBezout.gcd but maybe it's better to allow a separate GCDMonoid instance and use that gcd so the lemmas won't just apply to the particular choice of gcd/generators.

Indeed most lemmas about IsRelPrime has coprime in their names instead. I think we have to use a new name (and IsRelPrime) is my choice, since IsCoprime is widely used and we'd like to deprecate it rather than renaming it right away. I won't rename the lemmas so that they have the right names when we later rename IsRelPrime back to IsCoprime. (But do we need to deprecate IsRelPrime then? Maybe it's better to rename IsCoprime right now ...)

I still think IsComaximal is a reasonable name, since IsCoprime x y is equivalent to the comaximality (currently with the unintuitive name Codisjoint) of the ideals they generate, and also to the comaximality of the basic opens in the spectrum.

[jcommelin]

Thanks 🎉

bors merge

[mathlib-bors]

Pull request successfully merged into master.

Build succeeded:

• Build
• Check all files imported
• Lint style