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/Complex.thy
changeset 64272 f76b6dda2e56
parent 64267 b9a1486e79be
child 64290 fb5c74a58796 
--- a/src/HOL/Complex.thy	Mon Oct 17 14:37:32 2016 +0200
+++ b/src/HOL/Complex.thy	Mon Oct 17 17:33:07 2016 +0200
@@ -486,7 +486,7 @@
 lemma complex_cnj_mult [simp]: "cnj (x * y) = cnj x * cnj y"
   by (simp add: complex_eq_iff)
 
-lemma cnj_setprod [simp]: "cnj (setprod f s) = (\<Prod>x\<in>s. cnj (f x))"
+lemma cnj_prod [simp]: "cnj (prod f s) = (\<Prod>x\<in>s. cnj (f x))"
   by (induct s rule: infinite_finite_induct) auto
 
 lemma complex_cnj_inverse [simp]: "cnj (inverse x) = inverse (cnj x)"
isabelle