src/HOL/Groups_Big.thy

--- a/src/HOL/Groups_Big.thy	Sun Apr 08 12:31:08 2018 +0200
+++ b/src/HOL/Groups_Big.thy	Mon Apr 09 15:20:11 2018 +0100
@@ -1335,7 +1335,7 @@
   for f :: "'a \<Rightarrow> nat"
   using prod_zero_iff by (simp del: neq0_conv add: zero_less_iff_neq_zero)
 
-lemma prod_constant: "(\<Prod>x\<in> A. y) = y ^ card A"
+lemma prod_constant [simp]: "(\<Prod>x\<in> A. y) = y ^ card A"
   for y :: "'a::comm_monoid_mult"
   by (induct A rule: infinite_finite_induct) simp_all