[isabelle-dev] multiplicity and prime numbers

Manuel Eberl eberlm at in.tum.de
Tue Jul 19 14:43:41 CEST 2016

> 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"



More information about the isabelle-dev mailing list