equal
deleted
inserted
replaced
4 *) |
4 *) |
5 |
5 |
6 section \<open>Divisibility in monoids and rings\<close> |
6 section \<open>Divisibility in monoids and rings\<close> |
7 |
7 |
8 theory Divisibility |
8 theory Divisibility |
9 imports "~~/src/HOL/Library/Permutation" Coset Group |
9 imports "HOL-Library.Permutation" Coset Group |
10 begin |
10 begin |
11 |
11 |
12 section \<open>Factorial Monoids\<close> |
12 section \<open>Factorial Monoids\<close> |
13 |
13 |
14 subsection \<open>Monoids with Cancellation Law\<close> |
14 subsection \<open>Monoids with Cancellation Law\<close> |