equal
deleted
inserted
replaced
29 finally show "f (- x) = - f x" by (rule add_right_imp_eq) |
29 finally show "f (- x) = - f x" by (rule add_right_imp_eq) |
30 qed |
30 qed |
31 |
31 |
32 lemma (in additive) diff: "f (x - y) = f x - f y" |
32 lemma (in additive) diff: "f (x - y) = f x - f y" |
33 by (simp add: diff_def add minus) |
33 by (simp add: diff_def add minus) |
|
34 |
|
35 lemma (in additive) setsum: "f (setsum g A) = (\<Sum>x\<in>A. f (g x))" |
|
36 apply (cases "finite A") |
|
37 apply (induct set: finite) |
|
38 apply (simp add: zero) |
|
39 apply (simp add: add) |
|
40 apply (simp add: zero) |
|
41 done |
34 |
42 |
35 |
43 |
36 subsection {* Real vector spaces *} |
44 subsection {* Real vector spaces *} |
37 |
45 |
38 class scaleR = type + |
46 class scaleR = type + |