src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
changeset 45627 a0336f8b6558
parent 44890 22f665a2e91c
child 45630 0dd654a01217
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Nov 24 21:15:20 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Thu Nov 24 21:41:58 2011 +0100
     1.3 @@ -114,8 +114,8 @@
     1.4     (-1::int)^(card E) = (-1::int)^(nat(setsum (%x. ((x * a) div p)) A))"
     1.5  proof -
     1.6    assume "a \<in> zOdd"
     1.7 -  from QRLemma4 [OF this] have
     1.8 -    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" ..
     1.9 +  from QRLemma4 [OF this, symmetric] have
    1.10 +    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
    1.11    moreover have "0 \<le> int(card E)"
    1.12      by auto
    1.13    moreover have "0 \<le> setsum (%x. ((x * a) div p)) A"