Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I’m losing track of all the little recent edits I’ve made, but among them I created Euclidean domain, and added to principal ideal domain and unique factorization domain, proving the familiar inclusions between them. Piddled around a little with polynomial as well.
Is every Euclidean domain a principal ideal domain in constructive mathematics?
If every Euclidean domain is a principal ideal domain in constructive mathematics, does that mean that the integers are not an Euclidean domain? Because according to the principal ideal domain article, the integers aren’t a principal ideal domain.
This mathoverflow thread shows that every Euclidean domain is a unique factorization domain, avoiding principal ideal domains entirely, but I’m not sure if the proof is valid constructively.
The usual definition of unique factorization domain doesn’t seem to be constructively valid, see this Mathoverflow post.
changed higher algebra - contents to algebra - contents in context sidebar
Anonymouse
1 to 8 of 8