[isabelle-dev] multiplicity and prime numbers
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.
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