89 lemma scaleR_left_commute: |
89 lemma scaleR_left_commute: |
90 fixes x :: "'a::real_vector" |
90 fixes x :: "'a::real_vector" |
91 shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)" |
91 shows "scaleR a (scaleR b x) = scaleR b (scaleR a x)" |
92 by (simp add: mult_commute) |
92 by (simp add: mult_commute) |
93 |
93 |
94 lemma additive_scaleR_right: "additive (\<lambda>x. scaleR a x::'a::real_vector)" |
94 interpretation additive_scaleR_left: |
|
95 additive ["(\<lambda>a. scaleR a x::'a::real_vector)"] |
|
96 by (rule additive.intro, rule scaleR_left_distrib) |
|
97 |
|
98 interpretation additive_scaleR_right: |
|
99 additive ["(\<lambda>x. scaleR a x::'a::real_vector)"] |
95 by (rule additive.intro, rule scaleR_right_distrib) |
100 by (rule additive.intro, rule scaleR_right_distrib) |
96 |
101 |
97 lemma additive_scaleR_left: "additive (\<lambda>a. scaleR a x::'a::real_vector)" |
102 lemmas scaleR_zero_left [simp] = additive_scaleR_left.zero |
98 by (rule additive.intro, rule scaleR_left_distrib) |
103 |
99 |
104 lemmas scaleR_zero_right [simp] = additive_scaleR_right.zero |
100 lemmas scaleR_zero_left [simp] = |
105 |
101 additive.zero [OF additive_scaleR_left, standard] |
106 lemmas scaleR_minus_left [simp] = additive_scaleR_left.minus |
102 |
107 |
103 lemmas scaleR_zero_right [simp] = |
108 lemmas scaleR_minus_right [simp] = additive_scaleR_right.minus |
104 additive.zero [OF additive_scaleR_right, standard] |
109 |
105 |
110 lemmas scaleR_left_diff_distrib = additive_scaleR_left.diff |
106 lemmas scaleR_minus_left [simp] = |
111 |
107 additive.minus [OF additive_scaleR_left, standard] |
112 lemmas scaleR_right_diff_distrib = additive_scaleR_right.diff |
108 |
|
109 lemmas scaleR_minus_right [simp] = |
|
110 additive.minus [OF additive_scaleR_right, standard] |
|
111 |
|
112 lemmas scaleR_left_diff_distrib = |
|
113 additive.diff [OF additive_scaleR_left, standard] |
|
114 |
|
115 lemmas scaleR_right_diff_distrib = |
|
116 additive.diff [OF additive_scaleR_right, standard] |
|
117 |
113 |
118 lemma scaleR_eq_0_iff [simp]: |
114 lemma scaleR_eq_0_iff [simp]: |
119 fixes x :: "'a::real_vector" |
115 fixes x :: "'a::real_vector" |
120 shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)" |
116 shows "(scaleR a x = 0) = (a = 0 \<or> x = 0)" |
121 proof cases |
117 proof cases |