[isabelle-dev] Factorial ring

[Tjark Weber]

Florian,

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.

Best,
Tjark