equal
deleted
inserted
replaced
93 |
93 |
94 lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" |
94 lemma vector_uminus_component [simp]: "(- x)$i = - (x$i)" |
95 unfolding uminus_vec_def by simp |
95 unfolding uminus_vec_def by simp |
96 |
96 |
97 instance vec :: (semigroup_add, finite) semigroup_add |
97 instance vec :: (semigroup_add, finite) semigroup_add |
98 by default (simp add: vec_eq_iff add_assoc) |
98 by default (simp add: vec_eq_iff add.assoc) |
99 |
99 |
100 instance vec :: (ab_semigroup_add, finite) ab_semigroup_add |
100 instance vec :: (ab_semigroup_add, finite) ab_semigroup_add |
101 by default (simp add: vec_eq_iff add_commute) |
101 by default (simp add: vec_eq_iff add.commute) |
102 |
102 |
103 instance vec :: (monoid_add, finite) monoid_add |
103 instance vec :: (monoid_add, finite) monoid_add |
104 by default (simp_all add: vec_eq_iff) |
104 by default (simp_all add: vec_eq_iff) |
105 |
105 |
106 instance vec :: (comm_monoid_add, finite) comm_monoid_add |
106 instance vec :: (comm_monoid_add, finite) comm_monoid_add |