src/HOL/Groups_Big.thy
changeset 67969 83c8cafdebe8
parent 67683 817944aeac3f
child 68361 20375f232f3b
     1.1 --- a/src/HOL/Groups_Big.thy	Sun Apr 08 12:31:08 2018 +0200
     1.2 +++ b/src/HOL/Groups_Big.thy	Mon Apr 09 15:20:11 2018 +0100
     1.3 @@ -1335,7 +1335,7 @@
     1.4    for f :: "'a \<Rightarrow> nat"
     1.5    using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
     1.6  
     1.7 -lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
     1.8 +lemma prod_constant [simp]: "(\<Prod>x\<in> A. y) = y ^ card A"
     1.9    for y :: "'a::comm_monoid_mult"
    1.10    by (induct A rule: infinite_finite_induct) simp_all
    1.11