[isabelle-dev] Factorial ring
tjark.weber at it.uu.se
Fri Mar 11 13:39:48 CET 2016
On Thu, 2016-03-10 at 14:01 +0100, Manuel Eberl wrote:
> "multiplicity" is definitely interesting [...]
> I don't see why is_prime should require an algebraic_semidom [...]
> Factorial rings (also known as unique factorisation domains) usually
> [...] (somewhat non-standard) normalization_semidom.
My general impression is that it would be good if the algebraic
hierarchy that is part of standard Isabelle/HOL could follow standard
mathematical definitions and nomenclature more closely.
More information about the isabelle-dev