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


Cheers,

Manuel




More information about the isabelle-dev mailing list