Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Computational_Algebra/Primes.thy
changeset 73047 ab9e27da0e85
parent 69597 ff784d5a5bfb
child 73270 e2d03448d5b5 
--- a/src/HOL/Computational_Algebra/Primes.thy	Mon Jan 04 19:56:33 2021 +0100
+++ b/src/HOL/Computational_Algebra/Primes.thy	Mon Jan 04 19:41:38 2021 +0100
@@ -751,7 +751,7 @@
 
 lemma prime_factorization_prod_mset:
   assumes "0 \<notin># A"
-  shows "prime_factorization (prod_mset A) = \<Union>#(image_mset prime_factorization A)"
+  shows "prime_factorization (prod_mset A) = \<Sum>\<^sub>#(image_mset prime_factorization A)"
   using assms by (induct A) (auto simp add: prime_factorization_mult)
 
 lemma prime_factors_prod:
isabelle