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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
