The usual definition of unique factorization domain doesn’t seem to be constructively valid, see this Mathoverflow post.
]]>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.
]]>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.
]]>Is every Euclidean domain a principal ideal domain in constructive mathematics?
]]>Added a description of the Euclidean algorithm.
]]>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.
]]>