equal
deleted
inserted
replaced
11 Is only a vector space if restricted to lists of the same length.\<close> |
11 Is only a vector space if restricted to lists of the same length.\<close> |
12 |
12 |
13 text\<open>Multiplication with a scalar:\<close> |
13 text\<open>Multiplication with a scalar:\<close> |
14 |
14 |
15 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70) |
15 abbreviation scale :: "('a::times) \<Rightarrow> 'a list \<Rightarrow> 'a list" (infix "*\<^sub>s" 70) |
16 where "x *\<^sub>s xs \<equiv> map (( * ) x) xs" |
16 where "x *\<^sub>s xs \<equiv> map ((*) x) xs" |
17 |
17 |
18 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs" |
18 lemma scale1[simp]: "(1::'a::monoid_mult) *\<^sub>s xs = xs" |
19 by (induct xs) simp_all |
19 by (induct xs) simp_all |
20 |
20 |
21 subsection \<open>\<open>+\<close> and \<open>-\<close>\<close> |
21 subsection \<open>\<open>+\<close> and \<open>-\<close>\<close> |