equal
deleted
inserted
replaced
1295 apply (erule finite_induct) |
1295 apply (erule finite_induct) |
1296 apply (auto simp add: insert_Diff_if) |
1296 apply (auto simp add: insert_Diff_if) |
1297 apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a") |
1297 apply (subgoal_tac "f a * setprod f F / f a = setprod f F * f a / f a") |
1298 apply (erule ssubst) |
1298 apply (erule ssubst) |
1299 apply (subst times_divide_eq_right [THEN sym]) |
1299 apply (subst times_divide_eq_right [THEN sym]) |
1300 apply (auto simp add: mult_ac divide_self) |
1300 apply (auto simp add: mult_ac times_divide_eq_right divide_self) |
1301 done |
1301 done |
1302 |
1302 |
1303 lemma setprod_inversef: "finite A ==> |
1303 lemma setprod_inversef: "finite A ==> |
1304 ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> |
1304 ALL x: A. f x \<noteq> (0::'a::{field,division_by_zero}) ==> |
1305 setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1305 setprod (inverse \<circ> f) A = inverse (setprod f A)" |