equal
deleted
inserted
replaced
1 (* |
1 (* Title: Divisibility in monoids and rings |
2 Title: Divisibility in monoids and rings |
2 Author: Clemens Ballarin, started 18 July 2008 |
3 Author: Clemens Ballarin, started 18 July 2008 |
|
4 |
3 |
5 Based on work by Stephan Hohe. |
4 Based on work by Stephan Hohe. |
6 *) |
5 *) |
7 |
6 |
8 theory Divisibility |
7 theory Divisibility |
153 finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" . |
152 finally have ri': "a \<otimes> (b \<otimes> i) = \<one>" . |
154 |
153 |
155 from carr' li' ri' |
154 from carr' li' ri' |
156 show "a \<in> Units G" by (simp add: Units_def, fast) |
155 show "a \<in> Units G" by (simp add: Units_def, fast) |
157 qed |
156 qed |
|
157 |
158 |
158 |
159 subsection {* Divisibility and Association *} |
159 subsection {* Divisibility and Association *} |
160 |
160 |
161 subsubsection {* Function definitions *} |
161 subsubsection {* Function definitions *} |
162 |
162 |