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 *)
```