Timeline for Constructively correct notion of unique factorization domain
Current License: CC BY-SA 3.0
5 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Sep 22, 2016 at 11:59 | vote | accept | Ingo Blechschmidt | ||
| Sep 21, 2016 at 23:25 | answer | added | HeinrichD | timeline score: 7 | |
| Sep 21, 2016 at 18:53 | comment | added | Ingo Blechschmidt | @HeinrichD: Thanks! I'd be willing to accept this as an answer. You can show that the decomposition is unique by verifying that irreducible elements are prime; this is possible with Euclid's lemma (which holds in GCD domains and which admits a constructive proof). Furthermore, one can show that a domain is an UFD in their sense if and only if it is a UFD in the sense of my question and associatedness of irreducible elements is decidable. | |
| Sep 16, 2016 at 19:09 | comment | added | HeinrichD | It seems that Lombardi and Quitté in their book "Commutative Algebra: Constructive Methods" define UFDs as GCD-domains such that every regular element is a product of irreducibles (does this classically coincide with the usual definition, i.e. is the decomposition unique?). | |
| Dec 15, 2013 at 16:38 | history | asked | Ingo Blechschmidt | CC BY-SA 3.0 |