src/HOL/Number_Theory/Gauss.thy
changeset 58410 6d46ad54a2ab
parent 58288 87b59745dd6d
child 58645 94bef115c08f
     1.1 --- a/src/HOL/Number_Theory/Gauss.thy	Sun Sep 21 16:56:06 2014 +0200
     1.2 +++ b/src/HOL/Number_Theory/Gauss.thy	Sun Sep 21 16:56:11 2014 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4  
     1.5  subsection {* Gauss' Lemma *}
     1.6  
     1.7 -lemma aux: "setprod id A * -1 ^ card E * a ^ card A * -1 ^ card E = setprod id A * a ^ card A"
     1.8 +lemma aux: "setprod id A * (- 1) ^ card E * a ^ card A * (- 1) ^ card E = setprod id A * a ^ card A"
     1.9  by (metis (no_types) minus_minus mult.commute mult.left_commute power_minus power_one)
    1.10  
    1.11  theorem pre_gauss_lemma:
    1.12 @@ -363,7 +363,7 @@
    1.13      apply (rule cong_trans_int)
    1.14      apply (simp add: aux cong del:setprod.cong)
    1.15      done
    1.16 -  with A_prod_relprime have "[-1 ^ card E = a ^ card A](mod p)"
    1.17 +  with A_prod_relprime have "[(- 1) ^ card E = a ^ card A](mod p)"
    1.18      by (metis cong_mult_lcancel_int)
    1.19    then show ?thesis
    1.20      by (simp add: A_card_eq cong_sym_int)