[isabelle-dev] Factorial ring

[Manuel Eberl]

"multiplicity" is definitely interesting; we could then probably define 
the "order" of a root of a polynomial in terms of "multiplicity", which 
simplifies things a bit.

I don't see why is_prime should require an algebraic_semidom; the 
definition of prime elements makes sense in any commutative semiring.

Factorial rings (also known as unique factorisation domains) usually 
demand that any non-zero element can be written as a (finite) product of 
prime factors and a unit. This representation is necessarily unique 
modulo associativity/commutativity.

Intuitively, I would think that in a normalization_semidom, this implies 
that every non-zero element only has finitely many normalised divisors, 
but I am not completely sure about this. However, this would imply that 
your current definition is, in fact, equivalent to the standard 
mathematical one, at least in the context of the (somewhat non-standard) 
normalization_semidom.


Cheers,

Manuel