src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy
changeset 45630 0dd654a01217
parent 45627 a0336f8b6558
child 57418 6ab1c7cb0b8d
     1.1 --- a/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 10:52:30 2011 +0100
     1.2 +++ b/src/HOL/Old_Number_Theory/Quadratic_Reciprocity.thy	Fri Nov 25 13:14: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, symmetric] have
     1.8 -    "(int(card E): zEven) = (setsum (%x. ((x * a) div p)) A \<in> zEven)" .
     1.9 +  from QRLemma4 [OF this] 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"