changeset 67613 | ce654b0e6d69 |
parent 67399 | eab6ce8368fa |
child 68445 | c183a6a69f2d |
--- a/src/HOL/Algebra/UnivPoly.thy Tue Feb 13 14:24:50 2018 +0100 +++ b/src/HOL/Algebra/UnivPoly.thy Thu Feb 15 12:11:00 2018 +0100 @@ -284,7 +284,7 @@ lemma UP_l_neg_ex: assumes R: "p \<in> carrier P" - shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>" + shows "\<exists>q \<in> carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>" proof - let ?q = "\<lambda>i. \<ominus> (p i)" from R have closed: "?q \<in> carrier P"