# HG changeset patch # User paulson # Date 1610122054 0 # Node ID b69fd6e196623791481ef759d6ad035b27371fa3 # Parent 87067698ae53d5e97f95ffbd370d3408a9ccd964 One useful lemma/simprule diff -r 87067698ae53 -r b69fd6e19662 src/HOL/Computational_Algebra/Factorial_Ring.thy --- a/src/HOL/Computational_Algebra/Factorial_Ring.thy Fri Jan 08 15:13:23 2021 +0100 +++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy Fri Jan 08 16:07:34 2021 +0000 @@ -1606,6 +1606,9 @@ thus ?thesis by simp qed +lemma multiplicity_zero_1 [simp]: "multiplicity 0 x = 0" + by (metis (mono_tags) local.dvd_0_left multiplicity_zero not_dvd_imp_multiplicity_0) + lemma inj_on_Prod_primes: assumes "\P p. P \ A \ p \ P \ prime p" assumes "\P. P \ A \ finite P"