equal
deleted
inserted
replaced
1031 (setprod f (A - {a}) :: 'a :: {field}) = |
1031 (setprod f (A - {a}) :: 'a :: {field}) = |
1032 (if a:A then setprod f A / f a else setprod f A)" |
1032 (if a:A then setprod f A / f a else setprod f A)" |
1033 by (erule finite_induct) (auto simp add: insert_Diff_if) |
1033 by (erule finite_induct) (auto simp add: insert_Diff_if) |
1034 |
1034 |
1035 lemma setprod_inversef: |
1035 lemma setprod_inversef: |
1036 fixes f :: "'b \<Rightarrow> 'a::{field,division_ring_inverse_zero}" |
1036 fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero" |
1037 shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1037 shows "finite A ==> setprod (inverse \<circ> f) A = inverse (setprod f A)" |
1038 by (erule finite_induct) auto |
1038 by (erule finite_induct) auto |
1039 |
1039 |
1040 lemma setprod_dividef: |
1040 lemma setprod_dividef: |
1041 fixes f :: "'b \<Rightarrow> 'a::{field,division_ring_inverse_zero}" |
1041 fixes f :: "'b \<Rightarrow> 'a::field_inverse_zero" |
1042 shows "finite A |
1042 shows "finite A |
1043 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
1043 ==> setprod (%x. f x / g x) A = setprod f A / setprod g A" |
1044 apply (subgoal_tac |
1044 apply (subgoal_tac |
1045 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
1045 "setprod (%x. f x / g x) A = setprod (%x. f x * (inverse \<circ> g) x) A") |
1046 apply (erule ssubst) |
1046 apply (erule ssubst) |