src/HOL/Number_Theory/MiscAlgebra.thy
changeset 60773 d09c66a0ea10
parent 60527 eb431a5651fe
child 61952 546958347e05
     1.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jul 23 16:40:47 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jul 23 22:13:42 2015 +0200
     1.3 @@ -155,12 +155,12 @@
     1.4      and a [simp]: "a : carrier G"
     1.5    shows "a (^) card(carrier G) = one G"
     1.6  proof -
     1.7 -  have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
     1.8 +  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
     1.9      by (subst (2) finprod_reindex [symmetric],
    1.10        auto simp add: Pi_def inj_on_const_mult surj_const_mult)
    1.11 -  also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
    1.12 +  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
    1.13      by (auto simp add: finprod_multf Pi_def)
    1.14 -  also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
    1.15 +  also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
    1.16      by (auto simp add: finprod_const)
    1.17    finally show ?thesis
    1.18  (* uses the preceeding lemma *)