equal
deleted
inserted
replaced
53 apply (rule mult_mono) |
53 apply (rule mult_mono) |
54 apply (auto intro: setprod_nonneg) |
54 apply (auto intro: setprod_nonneg) |
55 done |
55 done |
56 |
56 |
57 (* FIXME: In Finite_Set there is a useless further assumption *) |
57 (* FIXME: In Finite_Set there is a useless further assumption *) |
58 lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: {division_ring_inverse_zero, field})" |
58 lemma setprod_inversef: "finite A ==> setprod (inverse \<circ> f) A = (inverse (setprod f A) :: 'a:: field_inverse_zero)" |
59 apply (erule finite_induct) |
59 apply (erule finite_induct) |
60 apply (simp) |
60 apply (simp) |
61 apply simp |
61 apply simp |
62 done |
62 done |
63 |
63 |