equal
deleted
inserted
replaced
7 theory Linearform |
7 theory Linearform |
8 imports Vector_Space |
8 imports Vector_Space |
9 begin |
9 begin |
10 |
10 |
11 text \<open> |
11 text \<open> |
12 A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals |
12 A \<^emph>\<open>linear form\<close> is a function on a vector space into the reals that is |
13 that is additive and multiplicative. |
13 additive and multiplicative. |
14 \<close> |
14 \<close> |
15 |
15 |
16 locale linearform = |
16 locale linearform = |
17 fixes V :: "'a::{minus, plus, zero, uminus} set" and f |
17 fixes V :: "'a::{minus, plus, zero, uminus} set" and f |
18 assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y" |
18 assumes add [iff]: "x \<in> V \<Longrightarrow> y \<in> V \<Longrightarrow> f (x + y) = f x + f y" |