Unique factorization domains

[tirix]

Adds a few theorems about unique factorization domains (UFD), especially, ~1arithufd, the existence of a factorization into primes. Since the definition in set.mm is based on Kaplansky's characterization, this is not the definition but a property.

[savask]

All very minor nitpicks, and nice work as always!

I must admit I have already lost a sense of direction a little bit, is this work on UFDs related to the doubling the cube work?

[savask]

This is a very minor nitpick which can be safely ignored, but it's better to choose whether we hyphenate non- or not. I.e. write "nonunit, nonzero" or "non-unit, non-zero".

[tirix]

There are 623 instances of "nonzero", and only 34 instances of "non-zero" in set.mm right now, so I suppose we go for "nonzero".
Note that In my recent trial (#4867), the spellchecker of would understand and accept "non-unit" as two different words, but "nonunit" was not in the dictionary.

[tirix]

In cc2150e, I chose to use "non-unit, non-zero", in order to be consistent within the comment, however I'm open to any suggestion. (nonunit seems to be a valid word in English)

[tirix]

Note that in the last commit, following very pertinent remarks from @langgerard, I also deleted ~ drngnidlr which was in fact redundant with ~ drngidl (while weaker!), and removed commutativity hypotheses from ~ drngmxidlr and ~ krullndrng. I don't know how to best attribute this contribution to Gérard, since it does not make sense to add a "Proof modification" tag.

[tirix]

I must admit I have already lost a sense of direction a little bit, is this work on UFDs related to the doubling the cube work?

Maybe I also lost direction myself!

Next step is to prove that the polynomial ( ( X ^ 3 ) - 2 ) is indeed the minimal polynomial for ( 2 ^c ( 1 / 3 ) ) when considering rationals.
By ~ irredminply, it suffices to prove that it's irreducible.

The standard proof of irreducibility uses reduction of the coefficients modulo a prime, either using Eisenstein's Criterion or directly. Then in order to move from irreducibility over the integers to irreducibility over the rationals, the standard proof uses Gauss's lemma.

Both Eisenstein's Criterion and Gauss's lemma have formulations with UFD: this is why I've been proving theorems around irreducibles, prime ideals, prime elements and UFD recently.

[savask]

The standard proof of irreducibility uses reduction of the coefficients modulo a prime, either using Eisenstein's Criterion or directly.

You could also prove that a cubic polynomial (over any field) is irreducible if and only if it has no roots. Then the claim for x^3 - 2 would follow from rtprmirr. The UFD work is still very important regardless of the proof strategy you choose, though.

[tirix]

You could also prove that a cubic polynomial (over any field) is irreducible if and only if it has no roots. Then the claim for x^3 - 2 would follow from rtprmirr. The UFD work is still very important regardless of the proof strategy you choose, though.

Yes, that would work! Thanks!

[wlammen]

I don't know how to best attribute this contribution to Gérard,

What about using the comment section, as in ax13lem1?

Thanks to Gerard Lang, whose ideas allowed several improvements.