equal
deleted
inserted
replaced
1 (* Title: HOL/Algebra/Divisibility.thy |
1 (* Title: HOL/Algebra/Divisibility.thy |
2 Author: Clemens Ballarin |
2 Author: Clemens Ballarin |
3 Author: Stephan Hohe |
3 Author: Stephan Hohe |
4 *) |
4 *) |
5 |
5 |
6 header {* Divisibility in monoids and rings *} |
6 section {* Divisibility in monoids and rings *} |
7 |
7 |
8 theory Divisibility |
8 theory Divisibility |
9 imports "~~/src/HOL/Library/Permutation" Coset Group |
9 imports "~~/src/HOL/Library/Permutation" Coset Group |
10 begin |
10 begin |
11 |
11 |