I agree in principle, but putting up a hierarchy of algebraic structures
within the constraints of Isabelle's type class system is tricky.
Additionally, sometimes adjustments have to be made since some things
that are natural in ‘regular’ mathematics are awkward to express in a
theorem prover.
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)
"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
