> By the way, in Milne's notes (https://www.jmilne.org/math/CourseNotes/FT.pdf) > page 7, it states a definition of Integral Domains that does not seem to > match with any of the theorems around > https://us.metamath.org/mpeuni/mmtheorems201.html#df-idom
The cancellation law condition is equivalent to the zero divisors one. The proof is short and sweet, but I don't see it in set.mm. Maybe you want to make dfdomn? -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/3UIPG7ODORGJ9.2FH4ZBQF1NSZB%40wilsonb.com.
