[isabelle-dev] Factorial ring

Tjark Weber 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 mailing list