equal
deleted
inserted
replaced
137 by (simp add: smult_r_distr) |
137 by (simp add: smult_r_distr) |
138 also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra |
138 also from facts smult_r_null have "... = \<ominus>\<^sub>2(a \<odot>\<^sub>2 x)" by algebra |
139 finally show ?thesis . |
139 finally show ?thesis . |
140 qed |
140 qed |
141 |
141 |
142 subsection {* Every Abelian Group is a $\mathbb{Z}$-module *} |
142 subsection {* Every Abelian Group is a Z-module *} |
|
143 |
|
144 (* Not all versions of pdflatex permit $\mathbb{Z}$ in bookmarks. *) |
143 |
145 |
144 text {* Not finished. *} |
146 text {* Not finished. *} |
145 |
147 |
146 constdefs |
148 constdefs |
147 INTEG :: "int ring" |
149 INTEG :: "int ring" |