src/HOL/Groups_Big.thy
changeset 60429 d3d1e185cd63
parent 60353 838025c6e278
child 60494 e726f88232d3
     1.1 --- a/src/HOL/Groups_Big.thy	Thu Jun 11 21:41:55 2015 +0100
     1.2 +++ b/src/HOL/Groups_Big.thy	Fri Jun 12 08:53:23 2015 +0200
     1.3 @@ -1155,7 +1155,7 @@
     1.4  
     1.5  lemma (in semidom_divide) setprod_diff1:
     1.6    assumes "finite A" and "f a \<noteq> 0"
     1.7 -  shows "setprod f (A - {a}) = (if a \<in> A then divide (setprod f A) (f a) else setprod f A)"
     1.8 +  shows "setprod f (A - {a}) = (if a \<in> A then setprod f A div f a else setprod f A)"
     1.9  proof (cases "a \<notin> A")
    1.10    case True then show ?thesis by simp
    1.11  next