equal
deleted
inserted
replaced
102 |
102 |
103 instance prod :: |
103 instance prod :: |
104 (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add .. |
104 (cancel_comm_monoid_add, cancel_comm_monoid_add) cancel_comm_monoid_add .. |
105 |
105 |
106 instance prod :: (group_add, group_add) group_add |
106 instance prod :: (group_add, group_add) group_add |
107 by default (simp_all add: prod_eq_iff diff_minus) |
107 by default (simp_all add: prod_eq_iff) |
108 |
108 |
109 instance prod :: (ab_group_add, ab_group_add) ab_group_add |
109 instance prod :: (ab_group_add, ab_group_add) ab_group_add |
110 by default (simp_all add: prod_eq_iff) |
110 by default (simp_all add: prod_eq_iff) |
111 |
111 |
112 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))" |
112 lemma fst_setsum: "fst (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. fst (f x))" |