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 |
143 |
144 text {* Not finished. *} |
144 text {* Not finished. *} |
145 |
145 |
146 constdefs |
146 constdefs |
147 INTEG :: "int ring" |
147 INTEG :: "int ring" |