equal
deleted
inserted
replaced
84 lemma negate_eq2: |
84 lemma negate_eq2: |
85 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- Numeral1) \<cdot> x = - x" |
85 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> (- Numeral1) \<cdot> x = - x" |
86 by (unfold is_vectorspace_def) simp |
86 by (unfold is_vectorspace_def) simp |
87 |
87 |
88 lemma negate_eq2a: |
88 lemma negate_eq2a: |
89 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> # -1 \<cdot> x = - x" |
89 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> -1 \<cdot> x = - x" |
90 by (unfold is_vectorspace_def) simp |
90 by (unfold is_vectorspace_def) simp |
91 |
91 |
92 lemma diff_eq2: |
92 lemma diff_eq2: |
93 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y" |
93 "is_vectorspace V \<Longrightarrow> x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> x + - y = x - y" |
94 by (unfold is_vectorspace_def) simp |
94 by (unfold is_vectorspace_def) simp |