[isabelle-dev] multiplicity and prime numbers

[Manuel Eberl]

> But is it possible to adapt all lemmas accordingly?  I could imagine
> that some statements use the fact that the support of multiplicity are
> the prime numbers.
Not really. Some facts will still require the primality assumption, e.g.

lemma prime_multiplicity_mult_distrib:
   assumes "is_prime_elem p" "x ≠ 0" "y ≠ 0"
   shows   "multiplicity p (x * y) = multiplicity p x + multiplicity p y"


Cheers,

Manuel