equal
deleted
inserted
replaced
5 |
5 |
6 theory Module |
6 theory Module |
7 imports Ring |
7 imports Ring |
8 begin |
8 begin |
9 |
9 |
10 section {* Modules over an Abelian Group *} |
10 section \<open>Modules over an Abelian Group\<close> |
11 |
11 |
12 subsection {* Definitions *} |
12 subsection \<open>Definitions\<close> |
13 |
13 |
14 record ('a, 'b) module = "'b ring" + |
14 record ('a, 'b) module = "'b ring" + |
15 smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70) |
15 smult :: "['a, 'b] => 'b" (infixl "\<odot>\<index>" 70) |
16 |
16 |
17 locale module = R: cring + M: abelian_group M for M (structure) + |
17 locale module = R: cring + M: abelian_group M for M (structure) + |
101 "module R M" |
101 "module R M" |
102 by (auto intro: moduleI R_cring is_abelian_group |
102 by (auto intro: moduleI R_cring is_abelian_group |
103 smult_l_distr smult_r_distr smult_assoc1) |
103 smult_l_distr smult_r_distr smult_assoc1) |
104 |
104 |
105 |
105 |
106 subsection {* Basic Properties of Algebras *} |
106 subsection \<open>Basic Properties of Algebras\<close> |
107 |
107 |
108 lemma (in algebra) smult_l_null [simp]: |
108 lemma (in algebra) smult_l_null [simp]: |
109 "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>" |
109 "x \<in> carrier M ==> \<zero> \<odot>\<^bsub>M\<^esub> x = \<zero>\<^bsub>M\<^esub>" |
110 proof - |
110 proof - |
111 assume M: "x \<in> carrier M" |
111 assume M: "x \<in> carrier M" |