"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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
