equal
deleted
inserted
replaced
21 |
21 |
22 |
22 |
23 subsection \<open>Vector space laws\<close> |
23 subsection \<open>Vector space laws\<close> |
24 |
24 |
25 text \<open> |
25 text \<open> |
26 A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with |
26 A \<^emph>\<open>vector space\<close> is a non-empty set \<open>V\<close> of elements from @{typ 'a} with the |
27 the following vector space laws: The set \<open>V\<close> is closed under addition and |
27 following vector space laws: The set \<open>V\<close> is closed under addition and scalar |
28 scalar multiplication, addition is associative and commutative; \<open>- x\<close> is |
28 multiplication, addition is associative and commutative; \<open>- x\<close> is the |
29 the inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of |
29 inverse of \<open>x\<close> wrt.\ addition and \<open>0\<close> is the neutral element of addition. |
30 addition. Addition and multiplication are distributive; scalar |
30 Addition and multiplication are distributive; scalar multiplication is |
31 multiplication is associative and the real number \<open>1\<close> is the neutral |
31 associative and the real number \<open>1\<close> is the neutral element of scalar |
32 element of scalar multiplication. |
32 multiplication. |
33 \<close> |
33 \<close> |
34 |
34 |
35 locale vectorspace = |
35 locale vectorspace = |
36 fixes V |
36 fixes V |
37 assumes non_empty [iff, intro?]: "V \<noteq> {}" |
37 assumes non_empty [iff, intro?]: "V \<noteq> {}" |
76 qed |
76 qed |
77 |
77 |
78 lemmas add_ac = add_assoc add_commute add_left_commute |
78 lemmas add_ac = add_assoc add_commute add_left_commute |
79 |
79 |
80 |
80 |
81 text \<open>The existence of the zero element of a vector space follows from the |
81 text \<open> |
82 non-emptiness of carrier set.\<close> |
82 The existence of the zero element of a vector space follows from the |
|
83 non-emptiness of carrier set. |
|
84 \<close> |
83 |
85 |
84 lemma zero [iff]: "0 \<in> V" |
86 lemma zero [iff]: "0 \<in> V" |
85 proof - |
87 proof - |
86 from non_empty obtain x where x: "x \<in> V" by blast |
88 from non_empty obtain x where x: "x \<in> V" by blast |
87 then have "0 = x - x" by (rule diff_self [symmetric]) |
89 then have "0 = x - x" by (rule diff_self [symmetric]) |